Ina Schaeffer - Integrating Formal Verification into the Model-based Development of Adaptive

Ort: Raum S2-02 /  E302
Datum und Zeit: Dienstag, 4. November 2008, 16:25-18:00 Uhr

Ina Schäfer, Technische Universität Kaiserslautern

Integrating Formal Verification into the Model-based Development of Adaptive Embedded Systems

Model-based development of adaptive embedded systems is an approach to deal with the increased complexity
adaptation imposes on system design. Integrating formal verification techniques into this design process provides
means to rigorously prove critical properties. However, most verification tools are based on foundational models,
e.g. automata, unable to express intuitive notions used in model-based development appropriately. Furthermore,
automatic methods such as model checking are only efficiently applicable to systems of limited sizes due to the
state-explosion problem. Our approach to alleviate these problems uses a semantics-based integration of model-based
development and formal verification for adaptive embedded systems allowing to capture design-level models at a high
level of abstraction. Verification complexity induced by the applied modelling concepts is reduced by verified model
transformations. These transformations include model slicing, data domain abstractions and compositional reasoning
techniques. The overall approach as well as the model transformations have been evaluated together with the
development of an adaptive vehicle stability control system.