Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
How Amazon Web Services uses formal methods
Newcombe C., Rath T., Zhang F., Munteanu B., Brooker M., Deardeuff M.  Communications of the ACM 58 (4): 66-73, 2015. Type: Article
Date Reviewed: Nov 19 2015

Formal methods are useful for providing irrefutable and credible evidence in the design and implementation of web service features. The use of formal specification and verification models in the design of adaptable complex systems for the rapidly changing conduct and growth of businesses is not straightforward. Beyond the standard techniques that industries use to verify the trustworthiness and security of systems, what are the practical and formal approaches to the design of reliable, complex real-world software such as public cloud services? Newcombe et al. address this nontrivial question by presenting the formal methods that design engineers at Amazon have used over the years to provide security and reliability in complex software systems.

The authors emphasize: (1) the consistent use of design and code reviews by systems engineers to provide robust security and fault-tolerance in complex systems; (2) the importance of selecting a relevant language for the formal design specification and verification of any complex system; (3) the use of an appropriate formal language for identifying elusive software defects, to help increase software performance without jeopardizing accuracy; (4) the benefits of using formal languages to provide safe and accurate responses in complex software; and (5) the ability to recognize the limitations of current formal models in predicting future behaviors in evolving software systems.

Clearly, the authors outline new challenges for the educators of future robust software system designers. Certainly, educators of future software engineers ought to be exposing students to the discrete mathematics and elements of set theory that are required for understanding formal design and specification languages. Future software engineers ought to understand the use of formal methods in the correct design and better implementation of complex systems. I encourage all complex software designers and educators to read and take advantage of the practical ideas in this article.

Reviewer:  Amos Olagunju Review #: CR143966 (1602-0124)
Bookmark and Share
  Reviewer Selected
Featured Reviewer
Testing And Debugging (D.2.5 )
Coding Tools and Techniques (D.2.3 )
General (K.6.0 )
General (C.2.0 )
General (D.3.0 )
Reliability (D.4.5 )
Would you recommend this review?
Other reviews under "Testing And Debugging": Date
Is the stack distance between test case and method correlated with test effectiveness?
Niedermayr R., Wagner S.  EASE 2019 (Proceedings of the Evaluation and Assessment on Software Engineering, Copenhagen, Denmark,  Apr 15-17, 2019) 189-198, 2019. Type: Proceedings
Mar 15 2021
Keeping master green at scale
Ananthanarayanan S., Ardekani M., Haenikel D., Varadarajan B., Soriano S., Patel D., Adl-Tabatabai A.  EuroSys 2019 (Proceedings of the Fourteenth EuroSys Conference 2019, Dresden, Germany,  Mar 25-28, 2019) 1-15, 2019. Type: Proceedings
Jun 15 2020
DeFlaker: automatically detecting flaky tests
Bell J., Legunsen O., Hilton M., Eloussi L., Yung T., Marinov D.  ICSE 2018 (Proceedings of the 40th International Conference on Software Engineering, Gothenburg, Sweden,  May 27-Jun 3, 2018) 433-444, 2018. Type: Proceedings
May 20 2020

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2022 ThinkLoud, Inc.
Terms of Use
| Privacy Policy