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 ACM58 (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
Software defect removal
Dunn R., McGraw-Hill, Inc., New York, NY, 1984. Type: Book (9789780070183131)
Mar 1 1985
On the optimum checkpoint selection problem
Toueg S., Babaoglu O. SIAM Journal on Computing 13(3): 630-649, 1984. Type: Article
Mar 1 1985
Software testing management
Royer T., Prentice-Hall, Inc., Upper Saddle River, NJ, 1993. Type: Book (9780135329870)
Mar 1 1994

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy