Reasoning Challenges for Guard Applications
Event details
| Date | 04.06.2012 |
| Hour | 14:00 › 15:00 |
| Speaker | Dr. Mike Whalen, University of Minnesota Software Engineering Center, USA |
| Location | |
| Category | Conferences - Seminars |
Abstract :
Guardol is a domain-specific language designed to facilitate the construction of correct network guards operating over tree-shaped data. The Guardol system generates Ada code from Guardol programs and also provides speci cation and automated veri cation support.
Guard programs and specications are translated to higher order logic, then deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data.
The result is that certain complex properties of Guardol programs can be proved fully automatically. Reasoning challenges for guards involve several aspects:
- Reasoning about tree structured data
- Reasoning about strings
- Reasoning about arrays
as well as language design to easily support such reasoning. In this talk we describe how some of these challenges have been addressed, and how several are yet to be addressed.
Bio :
Software plays an increasing role in the operation of critical systems. As these systems become more complex, ensuring software correctness becomes much more difficult. I am interested in automated formal techniques for precisely specifying, implementing, and verifying software. To support these activities, I have developed several translation and analysis tools to support formal reasoning and test case generation. I have significant experience in applying formal verification and auto-test generation techniques to production DO178B Level A and B avionics software development efforts.
I have 15 years experience in software development and analysis, including 10 years experience in Model-Based Development & safety-critical systems. Most of that time has been spent developing simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, Lustre, and RSML-e. I have 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). I 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.
I completed my PhD at the University of Minnesota in January, 2005. As a graduate student, I worked in the Critical Systems Research Group ( CriSys ), where I helped design a synchronous language called Requirements State Machine Language without Events (RSML-e). My Masters thesis provided the first complete formalization of RSML-e, written in the Z formalism. This formalization has formed the backbone of the RSML-e NIMBUS Simulator and translation tools from RSML-e to model checking and theorem proving tools. My PhD dissertation re-formalized RSML-e using higher-order abstract syntax and structural operational semantics to create a provably-correct translator from RSML-e to a subset of C.
Guardol is a domain-specific language designed to facilitate the construction of correct network guards operating over tree-shaped data. The Guardol system generates Ada code from Guardol programs and also provides speci cation and automated veri cation support.
Guard programs and specications are translated to higher order logic, then deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data.
The result is that certain complex properties of Guardol programs can be proved fully automatically. Reasoning challenges for guards involve several aspects:
- Reasoning about tree structured data
- Reasoning about strings
- Reasoning about arrays
as well as language design to easily support such reasoning. In this talk we describe how some of these challenges have been addressed, and how several are yet to be addressed.
Bio :
Software plays an increasing role in the operation of critical systems. As these systems become more complex, ensuring software correctness becomes much more difficult. I am interested in automated formal techniques for precisely specifying, implementing, and verifying software. To support these activities, I have developed several translation and analysis tools to support formal reasoning and test case generation. I have significant experience in applying formal verification and auto-test generation techniques to production DO178B Level A and B avionics software development efforts.
I have 15 years experience in software development and analysis, including 10 years experience in Model-Based Development & safety-critical systems. Most of that time has been spent developing simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, Lustre, and RSML-e. I have 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). I 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.
I completed my PhD at the University of Minnesota in January, 2005. As a graduate student, I worked in the Critical Systems Research Group ( CriSys ), where I helped design a synchronous language called Requirements State Machine Language without Events (RSML-e). My Masters thesis provided the first complete formalization of RSML-e, written in the Z formalism. This formalization has formed the backbone of the RSML-e NIMBUS Simulator and translation tools from RSML-e to model checking and theorem proving tools. My PhD dissertation re-formalized RSML-e using higher-order abstract syntax and structural operational semantics to create a provably-correct translator from RSML-e to a subset of C.
Links
Practical information
- General public
- Free
Organizer
- SuRI 2012
Contact
- Simone Muller