Chris Newcombe
Abstract
Engineers use TLA+ to prevent serious but subtle bugs from reaching production.
- Abrial, J. Formal methods in industry: Achievements, problems, future. In Proceedings of the 28th International Conference on Software Engineering (Shanghai, China, 2006), 761--768. Google Scholar
Digital Library
- Amazon.com. Supported Operations in DynamoDB: Strongly Consistent Reads. System documentation; http://docs.aws.amazon.com/amazondynamodb/latest/developerguide/APISummary.htmlGoogle Scholar
- Barr, J. Amazon S3: The first trillion objects. Amazon Web Services Blog, June 2012; http://aws.typepad.com/aws/2012/06/amazon-s3-the-first-trillion-objects.htmlGoogle Scholar
- Barr, J. Amazon S3: Two trillion objects, 1.1 million requests per second. Amazon Web Services Blog, Mar. 2013; http://aws.typepad.com/aws/2013/04/amazons3-two-trillion-objects-11-million-requests-second.htmlGoogle Scholar
- Batson, B. and Lamport, L. High-level specifications: Lessons from industry. In Formal Methods for Components and Objects, Lecture Notes in Computer Science Number 2852, F.S. de Boer, M. Bonsangue, S. Graf, and W.-P. de Roever, Eds. Springer, 2003, 242--262.Google ScholarCross Ref
- Bolosky, W., Douceur, J., and Howell, J. The Farsite Project: A retrospective. ACM SIGOPS Operating Systems Review: Systems Work at Microsoft Research 41, 2 (Apr. 2007), 17--26. Google ScholarDigital Library
- Brooker, M. Exploring TLA+ with two-phase commit. Personal blog, Jan. 2013; http://brooker.co.za/blog/2013/01/20/two-phase.htmlGoogle Scholar
- Holloway, C. Michael Why you should read accident reports. Presented at the Software and Complex Electronic Hardware Standardization Conference (Norfolk, VA, July 2005); http://klabs.org/richcontent/conferences/faa_nasa_2005/presentations/cmh-why-read-accident-reports.pdfGoogle Scholar
- Joshi, R., Lamport, L. et al. Checking cache-coherence protocols with TLA+. Formal Methods in System Design 22, 2 (Mar, 2003) 125--131. Google ScholarDigital Library
- Kudrjavets, G., Nagappan, N., and Ball, T. Assessing the relationship between software assertions and code quality: An empirical investigation. In Proceedings of the 17th International Symposium on Software Reliability Engineering (Raleigh, NC, Nov. 2006), 204--212. Google ScholarDigital Library
- Lamport, L. The TLA Home Page; http://research.microsoft.com/en-us/um/people/lamport/tla/tla.htmlGoogle Scholar
- Lamport, L. Fast Paxos. Distributed Computing 19, 2 (Oct. 2006), 79--103.Google ScholarDigital Library
- Lamport, L. The Wildfire Challenge Problem; http://research.microsoft.com/en-us/um/people/lamport/tla/wildfire-challenge.htmlGoogle Scholar
- Lamport, L. Checking a multithreaded algorithm with +CAL. In Distributed Computing: 20th International Conference, S. Dolev, Ed. Springer-Verlag, 2006, 11--163. Google ScholarDigital Library
- Lamport, L. and Merz, S. Specifying and verifying fault-tolerant systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science, Number 863, H. Langmaack, W.-P. de Roever, and J. Vytopil, Eds. Springer-Verlag, Sept. 1994, 41--76. Google ScholarDigital Library
- Lamport, L., Sharma, M., Tuttle, M., and Yu, Y. The Wildfire Challenge Problem. Jan. 2001; http://research.microsoft.com/en-us/um/people/lamport/pubs/wildfire-challenge.pdfGoogle Scholar
- Lu, T., Merz, S., and Weidenbach, C. Towards verification of the Pastry Protocol using TLA+. In Proceedings of Joint 13th IFIP WG 6.1 International Conference and 30th IFIP WG 6.1 International Conference Lecture Notes in Computer Science Volume 6722 (Reykjavik, Iceland, June 6--9). Springer-Verlag, 2011, 244--258. Google ScholarDigital Library
- Newcombe, C. Debugging Designs. Presented at the 14th International Workshop on High-Performance Transaction Systems (Monterey, CA, Oct. 2011); http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf and associated specifications http://hpts.ws/papers/2011/sessions_2011/amazonbundle.tar.gzGoogle Scholar
- Newcombe, C. Why Amazon chose TLA+. In Proceedings of the Fourth International Conference Lecture Notes in Computer Science Volume 8477, Y.A. Ameur and K.-D. Schewe, Eds. (Toulouse, France, June 2--6). Springer, 2014, 25--39.Google Scholar
- Patterson, D., Fox, A. et al. The Berkeley/Stanford Recovery-Oriented Computing Project. University of California, Berkeley; http://roc.cs.berkeley.edu/Google Scholar
- Tasiran, S., Yu, Y., Batson, B., and Kreider, S. Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor. In Proceedings of the Third IEEE International Workshop on Microprocessor Test and Verification (Austin, TX, June). IEEE Computer Society, 2002.Google Scholar
- Zave, P. Using lightweight modeling to understand Chord. ACM SIGCOMM Computer Communication Review 42, 2 (Apr. 2012), 49--57. Google ScholarDigital Library
Index Terms
- How Amazon web services uses formal methods
Recommendations
Formal Methods for Data-centric Web Services: From Model to Implementation
ICWS '13: Proceedings of the 2013 IEEE 20th International Conference on Web ServicesWeb services allow organizations to capture their human and software-based capabilities as modular software components that are called remotely over a network. In such service-oriented settings, it is important to establish an agreement that sets the ...
Reviews
Amos O Olagunju
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. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments