Invited Talks
Model-Based Verification of Automotive Control Software
Rance Cleaveland
Department of Computer Science and Fraunhofer USA Center for Experimental Software Engineering University of Maryland (FME keynote speaker)
Abstract.
This talk will report on the use of an approach, called Instrumentation-Based Verification, for checking the correctness of models of control software given in Simulink® and Stateflow®. In IBV, engineers formalize requirements as so-called monitor models, whose purpose is to search executions of the main controller model for violations of required behavior. Testing is then performed on the instrumented controller model in order to check for the possibility of deviations between controller and requirements. Tools such as Reactis® provide automated support for conducting these activities, and the technique has attracted interest in automotive, aerospace and medical-device settings.
The presentation will first review model-based development and IBV and their industrial motivations. It will then report on a project between the Fraunhofer Center for Experimental Software Engineering and a major automotive supplier on using IBV to verify models of an exterior-lighting control system.
This talk will report on the use of an approach, called Instrumentation-Based Verification, for checking the correctness of models of control software given in Simulink® and Stateflow®. In IBV, engineers formalize requirements as so-called monitor models, whose purpose is to search executions of the main controller model for violations of required behavior. Testing is then performed on the instrumented controller model in order to check for the possibility of deviations between controller and requirements. Tools such as Reactis® provide automated support for conducting these activities, and the technique has attracted interest in automotive, aerospace and medical-device settings.
The presentation will first review model-based development and IBV and their industrial motivations. It will then report on a project between the Fraunhofer Center for Experimental Software Engineering and a major automotive supplier on using IBV to verify models of an exterior-lighting control system.
Biography:
Rance Cleaveland is Professor of Computer Science at the University of Maryland at College Park, where he is also Executive and Scientific Director of the Fraunhofer USA Center for Experimental and Software Engineering. Prior to joining the Maryland faculty in 2005, he held professorships at the State University of New York at Stony Brook and at North Carolina State University. He also co-founded Reactive Systems, Inc., in 1999 to commercialize tools for model-based testing of embedded software; Reactive Systems currently has customers worldwide in the automotive and aerospace industries. In 1992 he received Young Investigator Awards from the US National Science Foundation and from the US Office of Naval Research, and in 1994 he was awarded the Alcoa Engineering Research Achievement prize at North Carolina State University. He has published over 100 papers in the areas of software verification and validation, formal methods, model checking, software specification formalisms, and verification tools. Cleaveland received B.S. degrees in Mathematics and Computer Science from Duke University in 1982 and his M.S. and Ph.D. degrees from Cornell University in 1985 and 1987 respectively. He is a member of IEEE, the Association for Computing Machinery, and the Society for Automotive Engineering.
Rance Cleaveland is Professor of Computer Science at the University of Maryland at College Park, where he is also Executive and Scientific Director of the Fraunhofer USA Center for Experimental and Software Engineering. Prior to joining the Maryland faculty in 2005, he held professorships at the State University of New York at Stony Brook and at North Carolina State University. He also co-founded Reactive Systems, Inc., in 1999 to commercialize tools for model-based testing of embedded software; Reactive Systems currently has customers worldwide in the automotive and aerospace industries. In 1992 he received Young Investigator Awards from the US National Science Foundation and from the US Office of Naval Research, and in 1994 he was awarded the Alcoa Engineering Research Achievement prize at North Carolina State University. He has published over 100 papers in the areas of software verification and validation, formal methods, model checking, software specification formalisms, and verification tools. Cleaveland received B.S. degrees in Mathematics and Computer Science from Duke University in 1982 and his M.S. and Ph.D. degrees from Cornell University in 1985 and 1987 respectively. He is a member of IEEE, the Association for Computing Machinery, and the Society for Automotive Engineering.
Contract-Based Analysis of automotive and avionics applications: the SPEEDS Approach
Werner Damm
OFFIS, Germany
Abstract
The Speeds project has developed a layered meta-model of heterogeneous rich components and standardized approaches for the integration of commercial industry standard modeling tools to assemble system-level design models with contract-baed interface specifications by combining models expressed in any authoring tool compliant to the integration standard, including Matlab-Simulink/Stateflow, Rhapsody, and Scade. It is currently integrating a range of analysis methods supporting interface compliance testing and dominance analysis between contracts expressed in extended automata model, subsuming timed automata. The presentation focuses on real-time analysis methods, and demonstrates a methodology for assessing realizability of end-to-end latencies at system level, exploring the design space of possible system configurations meeting vertical resource assumptions, and assessing compliance to such vertical assumptions based on distributed real-time schedulability analysis for FlexRay and CAN bus based target architectures.
The Speeds project has developed a layered meta-model of heterogeneous rich components and standardized approaches for the integration of commercial industry standard modeling tools to assemble system-level design models with contract-baed interface specifications by combining models expressed in any authoring tool compliant to the integration standard, including Matlab-Simulink/Stateflow, Rhapsody, and Scade. It is currently integrating a range of analysis methods supporting interface compliance testing and dominance analysis between contracts expressed in extended automata model, subsuming timed automata. The presentation focuses on real-time analysis methods, and demonstrates a methodology for assessing realizability of end-to-end latencies at system level, exploring the design space of possible system configurations meeting vertical resource assumptions, and assessing compliance to such vertical assumptions based on distributed real-time schedulability analysis for FlexRay and CAN bus based target architectures.
Biography:
Prof. Werner Damm holds the Chair for Safety Critical Embedded Systems at the Carl von Ossietzky University of Oldenburg. He is member of the Board of Directors of OFFIS, the Chairman of the SafeTRANS competence cluster, integrating leading companies and research institutes in the transportation domain, Chairman of the Steering Board of EICOSE (European Institute for Complex Safety Critical Systems Engineering), - the Artemis Innovation Cluster on Transportation - , member of the Artemis Working Group on Innovation as well as of the ITEA2 Roadmap Steering Board. Prof. Damm is a co-founder and member of the board of directors of OSC Embedded Systems AG. He has served in advisory committees of the Max Planck Society and the Humboldt University Berlin, he is the Scientific Director of the Transregional Collaborative Research Center AVACS (SFB/TR 14 Automatic Verification and Analysis of Complex Systems) and is the Director of the Interdisciplinary Research Center on Safety Critical Systems of the Carl von Ossietzky Universität Oldenburg. His recent research covers foundational research on mathematical models of embedded systems, specification languages, hybrid systems, formal verification methods, and real-time and safety analysis. This is complemented by applied research with industrial partners in avionics, automotive, and train system application. The focus of this research is on enhancing model-based development processes with formal method-based approaches to verification, testing, and safety and real-time analysis, as well as on enabling component-based design for embedded systems.
Prof. Werner Damm holds the Chair for Safety Critical Embedded Systems at the Carl von Ossietzky University of Oldenburg. He is member of the Board of Directors of OFFIS, the Chairman of the SafeTRANS competence cluster, integrating leading companies and research institutes in the transportation domain, Chairman of the Steering Board of EICOSE (European Institute for Complex Safety Critical Systems Engineering), - the Artemis Innovation Cluster on Transportation - , member of the Artemis Working Group on Innovation as well as of the ITEA2 Roadmap Steering Board. Prof. Damm is a co-founder and member of the board of directors of OSC Embedded Systems AG. He has served in advisory committees of the Max Planck Society and the Humboldt University Berlin, he is the Scientific Director of the Transregional Collaborative Research Center AVACS (SFB/TR 14 Automatic Verification and Analysis of Complex Systems) and is the Director of the Interdisciplinary Research Center on Safety Critical Systems of the Carl von Ossietzky Universität Oldenburg. His recent research covers foundational research on mathematical models of embedded systems, specification languages, hybrid systems, formal verification methods, and real-time and safety analysis. This is complemented by applied research with industrial partners in avionics, automotive, and train system application. The focus of this research is on enhancing model-based development processes with formal method-based approaches to verification, testing, and safety and real-time analysis, as well as on enabling component-based design for embedded systems.
Formal Methods for Critical Systems
Steven P. Miller
Rockwell Collins
Abstract
Formal methods have traditionally been reserved for systems with requirements for extremely high assurance. However, the growing popularity of model-based development, in which models of system behavior are created early in the development process and used to auto-generate code, are making precise, mathematical specifications much more common in industry. At the same time, formal verification tools such as model checkers continue to grow more powerful. The convergence of these two trends opens the door for the practical application of formal verification techniques early in the life cycle for many systems. This talk will describe how Rockwell Collins has applied both theorem proving and model checking to commercial avionics and security systems to reduce costs and improve quality.
Formal methods have traditionally been reserved for systems with requirements for extremely high assurance. However, the growing popularity of model-based development, in which models of system behavior are created early in the development process and used to auto-generate code, are making precise, mathematical specifications much more common in industry. At the same time, formal verification tools such as model checkers continue to grow more powerful. The convergence of these two trends opens the door for the practical application of formal verification techniques early in the life cycle for many systems. This talk will describe how Rockwell Collins has applied both theorem proving and model checking to commercial avionics and security systems to reduce costs and improve quality.
Biography:
Dr. Steven Miller is a Senior Principal Software Engineer in the Advanced Technology Center of Rockwell Collins. He has over 30 years of experience in software development for both mainframe and embedded systems. He received his Ph.D. in computer science from the University of Iowa in 1991, and also holds a B.A. in physics and mathematics from the University of Iowa. His current research interests include model-based development and formal methods. He was principle investigator on a 5-year project sponsored by NASA Langley's Aviation Safety Program and Rockwell Collins to investigate advanced methods and tools for the development flight critical systems. Prior to that he lead several research efforts at Rockwell Collins, including a collaborative effort with SRI International and NASA to formally verify the microcode in the AAMP5 and AAMP-FV microprocessors using the PVS verification system.
Dr. Steven Miller is a Senior Principal Software Engineer in the Advanced Technology Center of Rockwell Collins. He has over 30 years of experience in software development for both mainframe and embedded systems. He received his Ph.D. in computer science from the University of Iowa in 1991, and also holds a B.A. in physics and mathematics from the University of Iowa. His current research interests include model-based development and formal methods. He was principle investigator on a 5-year project sponsored by NASA Langley's Aviation Safety Program and Rockwell Collins to investigate advanced methods and tools for the development flight critical systems. Prior to that he lead several research efforts at Rockwell Collins, including a collaborative effort with SRI International and NASA to formally verify the microcode in the AAMP5 and AAMP-FV microprocessors using the PVS verification system.
