Read an article “How Amazon uses formal methods”

Introduction

This post summarizes experiences Amazon has gained, when using TLA+ specification tools, and discusses, what is needed to start using formal methods in business IT development context

Table of Contents

• Introduction
• How Amazon Web Services Uses Formal Methods
• Are formal methods really applicable in mainstream software development
• Changes
• Fin

How Amazon Web Services Uses Formal Methods

The article starts with presenting key insights by Amazon on using formal methods

• formal methods are surprisingly feasible for mainstream software development, and give good return on investment
• formal methods are routinely applied to the design of complex real-world software

It then explains experiences Amazon has gained, when using TLA+ specification tools, and an accompanied C-style programming language PlusCal.

In Amazon, the process starts by specifying what the system should do using correctness properties, followed by an abstract version of the design. This design is further refined into a specification, which can be verified using TLA+ tool model checker.

Amazon finds using formal methods helpful in many ways: “Get design right”, “Gain better understanding”, “Write better code”, and to bring benefits over the lifetime of the system, when a product needs to be changed.

Again, this approach is not a “silver bullet”, and the article adds a Word of Warning “All models are wrong, some are useful”.

Are formal methods really applicable in mainstream software development

as Amazon explains?

To me “mainstream software development” means developing business IT systems, where system architecture identifies

• interfaces: entry point providing access to services within the system,
• services: unit of functionality accessible over interfaces.
• database: persistent data store, which services may access, and modify.

To be applicable all relevant stakeholder should find an approach useful. In business IT development context, Business Owner, IT Architect, and IT Developer should find benefits like the ones summarized in the table below.

Business Owner	IT Architect	IT Developer
Maintain high ROI on IT investments	Maintain intellectual ownership of IT systems	Help in implementing relevant solutions for the business
Better business/IT alignment	Communication support	Get better implementation blueprints
Reduced IT risks	Tool support to manage architecture design

In order to help achieving benefits listed above, a workable solution should include (at least) the functions:

1. We may assume that we have an interface specification in a machine readable form. We should be able to take an interface specification, and use it to generate automatically runnable specification code.
2. Interface specifications typically define interface parameter data types without formally specifying their meaning. The solution should allow us to add meaning to interface parameters – a prerequisite before we can start defining criteria on correctness, or to model system behavior.
3. State space explosion is inherent problem in model checking, the theory behind TLA+ tool. The solution should allow us to avoid problems due to state space explosion.
4. The solution should have a code repository to store specification snippets needed to model system behavior, and correctness criteria. Assets in the code repository should be easy to include into the resulting specification code for model checking.
5. In any reasonable size business IT system, the volume of code snippets needed to model the system is going to be quite large. The solution should allow us to avoid problems caused by large specification code volume.
6. The solution should include functions for an architect to communicate implementation blueprints to a development team.

Changes

• 2018-02-05: Fixed link to article abstract

Fin

The next post presents Sbuilder (aka. Specificatio Builder), and how it addresses the requirements listed above.