The RE and formal methods research community has touted formal languages and tools to help improve requirements, system modeling, and checking implementation conformance. While there have been successful applications of formal methods in hardware design and aerospace, despite 50 years of research and development, we have not seen wide adoption of formal techniques for large and complex systems such as web services, industrial automation, or enterprise support software. Two key difficulties for using automated reasoning for these systems continue to involve eliciting and explaining requirements with customers and creating accurate system architectural models necessary to support analysis. With the cloud, much of this has changed. For requirements, we can work backwards from common pain points for a large community of users, propose solutions, and quickly iterate to better address user needs. In addition, descriptions of cloud services provide accurate models in the form of computer-readable contracts. These contracts establish and govern how the system behaves and in many cases they are amenable to formal analysis at scale. Most importantly, since those models are used by a large user community, it is now economically feasible to build the tools needed to verify those models. In this talk, we discuss the trend of constructing practical and scalable cloud-based formal methods at Amazon Web Services and how they can easily be used by customers – sometimes with just one-click.

Michael Whalen is a Principal Software Engineer at Amazon Web Services, where he works in the Automated Reasoning Group (ARG) applying proof techniques towards security applications. He is also an adjunct professor at the University of Minnesota where he was formerly the Director of the University of Minnesota Software Engineering Center (UMSEC).

Dr. Whalen is interested in formal analysis, language translation, testing, and requirements engineering. He has developed simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, SCADE, and RSML-e, and has published more than 90 papers on these topics. He has led successful formal verification projects on large industrial avionics models, including displays (Rockwell-Collins ADGS-2100 Window Manager), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program). He is currently working on improving the scalability of formal verification and extracting information from proofs that can be used to satisfy certification requirements related to traceability and adequacy of requirements. He has recently applied proof tools towards creating secure autonomous vehicles in the DARPA HACMS project.