Formal Modeling and Analysis of Software Systems with Lustre

Abstract:

Rockwell Collins and the University of Minnesota have used the synchronous dataflow language Lustre as a basis for a variety of analyses of industrial critical systems both for component level models written in Simulink and system architectural models written in AADL. This talk describes the approach, several examples of analyzed models as well as several challenges to extend the scale and variety of systems that can be practically analyzed.

Presentation Slides   (pptx)

Biography:

Michael Whalen is the Program Director at the University of Minnesota Software Engineering Center. He has 15 years experience in software development and analysis, including 10 years experience in Model-Based Development & safety-critical systems. Dr. Whalen has developed simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, Lustre, and RSML-e. 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). Dr. Whalen was the lead developer of the Rockwell-Collins Gryphon tool suite, which can be used for compilation, test-case generation, and formal analysis of Simulink/Stateflow models. This tool suite has been used both for academic research and industrial verification projects. Dr. Whalen is a frequent speaker and author on the use of formal methods, with 23 invited presentations, five journal publications, one book chapter, 24 conference papers, and 7 contractor and technical reports published. His PhD dissertation involved using higher-order abstract syntax as a basis for a provably-correct code generation tool from the RSML-e specification language into a subset of C. His interests include novel uses of model checking, test generation, theorem proving, and random search simulation tools to reduce the cost and manual effort required for systems and software validation for critical systems.