Slicing for Model Reduction in Adaptive Embedded Systems Development

Model-based development of adaptive embedded systems is an approach to deal with the increased complexity that adaptation requirements impose on system design. Integrat-ing formal verification techniques into this design process provides means to rigorously prove critical properties. How-ever, most automatic verification techniques such as model checking are only effectively applicable to systems of lim-ited sizes due to the state-explosion problem. Our approach to alleviate this problem consists of (a) a semantics-based integration of model-based development and formal verifi-cation for adaptive embedded systems and (b) an automatic slicing technique of models with respect to properties to be verified. Slicing is carried out on a high-level formal in-termediate representation of the models providing a clear separation of functional and adaptation behaviour. The in-ternal model structure can be exploited to identify system parts that are irrelevant for a property. In particular, slicing offers efficient model reductions for the verification of prop-erties of the adaptation behaviour. The overall approach and the slicing techniques have been evaluated together with the development of an adaptive vehicle stability control system