Campus Event Calendar
Event Entry
What and Who
Integrating Formal Verification into the Model-based Development of Adaptive Embedded Systems
Ina Schaefer
TU Kaiserslautern
SWS Colloquium
AG 2, SWS, RG1
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 17 July 2008
14:00
60 Minutes
E1 5
007
Saarbrücken
Abstract
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
providesmeans 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 integrationof 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 syste
deal with the increased complexity adaptation imposes on system design.
Integrating formal verification techniques into this design process
providesmeans 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 integrationof 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 syste
Contact
Claudia Richter
9325 688
--email hidden
passcode not visible
logged in users only
Claudia Richter, 07/16/2008 10:41 -- Created document.