Slicing for Model Reduction in Adaptive Embedded Systems Development

In: Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2008), Leipzig, Germany. May, 2008

Authors

• Ina Schaefer
• Arnd Poetzsch-Heffter

Abstract

Model-based development of adaptive embedded systems is an approach to deal with the increased complexity that adaptation requirements impose on system design. Integrating formal verification techniques into this design process provides means to rigorously prove critical properties. However, most automatic verification techniques such as model checking are only effectively applicable to systems of limited 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 verification for adaptive embedded systems and (b) an automatic slicing technique of models with respect to properties to be verified. The slicing is carried out on a high-level formal intermediate representation of the models. It allows using the internal model structure to identify system parts that are irrelevant to show a property. Furthermore, this technique facilitates slicing models in different granularity permitting a fine-grained control of necessary reductions for the applied verification tools. The overall approach and the slicing technique have been evaluated together with the development of an adaptive vehicle stability control system.

BibTeX

 
@InProceedings{ SchaeferPH.08, 
   title = { Slicing for Model Reduction in Adaptive Embedded Systems Development }, 
   author = { Ina Schaefer and Arnd Poetzsch-Heffter },   
   booktitle = { Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2008), Leipzig, Germany },             
   month = may, 
   year = 2008, 
} 

---

This publication belongs to the project EVAS.