Abstract* (max 1000 chars)

Amazon has been using the TLA+ specification language to great effect on their AWS services since 2011. We are interested in developing concise and complete descriptions of Openstack services. Using a formal specification language will let us unambiguously formulate an answer to, "Is this how Openstack should behave?" and verify that our designs do not lead to inconsistencies. Let's talk about specification languages, modeling, and formal methods!

What is the problem or use case you’re addressing in this session?* (max 1000 chars)

Operating Openstack in a public cloud has led to the discovery of some situations where the specifications at specs.openstack.org do not provide a concise and unambigious description of how a given service should behave and whether that behavior itself contains any inconsistencies in its design. We hope to find like-minded individuals who are interested in formal specification methods to talk about how we can bring these methods to open-source projects and improve Openstack.

It is our hope that high-level, mathematically sound specifications of Openstack services will also provide other benefits like allowing us to chase aggressive optimizations while maintaining correctness and reliability.

What should attendees expect to learn?* (max 1000 chars)

They will learn about formal methods, high-level specifications, and mathematical modeling.

Why should this session be selected?* (max 1000 chars)

It should be selected because we hope it will start a conversation about more formal ways to specify Openstack services and improve the quality of the software in terms of correctness, clarity, performance, and reliability. My colleague and I are not ready for a full presentation but we would like to meet with like-minded people to discuss these tools and ways we could integrate these methodologies in the community.