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 (C.2.0 )
General (D.3.0 )
General (K.6.0 )
Performance of Systems (C.4 )
Would you recommend this review?
Other reviews under "Testing And Debugging": Date
Take it or leave it: a survey study on operating system upgrade practices
Farhang S., Weidman J., Kamani M., Grossklags J., Liu P.  ACSAC 2018 (Proceedings of the 34th Annual Computer Security Applications Conference, San Juan, Puerto Rico,  Dec 3-7, 2018) 490-504, 2018. Type: Proceedings
Aug 19 2019
The quality of JUnit tests: an empirical study report
Ma’ayan D.  SQUADE 2018 (Proceedings of the 1st International Workshop on Software Qualities and Their Dependencies, Gothenburg, Sweden,  May 28, 2018) 33-36, 2018. Type: Proceedings
Jul 25 2019
Software fault detection and correction: modeling and applications
Peng R., Li Y., Liu Y.,  Springer International Publishing, New York, NY, 2018. 124 pp. Type: Book
May 30 2019

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