A system for programming and verifying interacting state machines

February 29, 2012
Damien Zufferey | Institute of Science and Technology Austria

We present a new development environment for programs composed of interacting state machines. It improves upon our previous work that enabled the formal development of the USB 3.0 device driver stack in Windows 8. The new programming environment provides easy specification and visualization of state machines, comprehensive verification early in the design process, and efficient code generation. We hope that these features would enable construction of reliable and correct asynchronous software systems. The verification capabilities of our system rest on two foundations—fast checking of syntactic properties via static analysis and potentially expensive checking of semantic properties via state exploration. After giving an overview of the system, we will focus on our effort to improve the scalability of state exploration through compositional verification. Our system allows the specification to be conjunctively decomposed into a collection of state machines. Each specification machine provides a partial description of the interaction among the implementation machines and is verified separately, perhaps by using other specification machines as lemmas. The compositional proof rule ensures soundness in spite of allowing circular use of lemmas. In the talk, we will give details of the compositional proof methodology and its implementation using declarative programming with Formula and model checking with Zing.

Speaker Bios

Damien Zufferey is a PhD student in Thomas A. Henzinger’s group at the Institute of Science and Technology Austria (IST Austria). He received a Master in computer science from EPFL in 2009, then he moved to IST Austria where he is working on verification of distributed systems. More specifically, he applies infinite-states model-checking techniques to mobile processes. His research interests range across program analysis, formal methods and programming languages. During the winter 2011-2012 he has done an internship at MSR in the RiSE group under supervision of Shaz Qadeer.