Correct design of asynchronous software
Dr. Sriram Rajamani
Recorded 11 September 2013 in Lausanne, Vaud, Switzerland
Asynchronous software is hard to design and get right. In this talk, I will talk about two approaches I have worked on (together with my collaborators) over the years. In the first part of my talk I will describe a verification approach where abstraction, model checking, theorem proving are used on existing code to verify certain critical properties. In the second part of my talk I will describe a design approach where the system is described as collection of asynchronous state machines, and verified at the design level, and then code is generated automatically from the design description. I will compare and contrast the pros and cons of the two approaches and our experience using both approaches.
Watched 454 times.Watch