Using Abstraction in Modular Verification of Synchronous Adaptive Systems
In: Proceedings of "Workshop on Trustworthy Software", Saarbrücken, May 18-19, 2006. Dagstuhl Online Proceedings , available at http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=699, May, 2006
Authors
- Ina Schaefer
- Arnd Poetzsch-Heffter
Abstract
Self-adaptive embedded systems autonomously adapt to changing environment conditions to improve their functionality and to increase their dependability by downgrading functionality in case of failures. However, adaptation behaviour of embedded systems significantly complicates system design and poses new challenges for guaranteeing system correctness, in particular vital in the automotive domain. Formal verification as applied in safety-critical applications must therefore be able to address not only temporal and functional properties, but also dynamic adaptation according to external and internal stimuli. In this paper, we introduce a formal semantic-based framework to model, specify and verify the functional and the adaptation behaviour of synchronous adaptive systems. The modelling separates functional and adaptive behaviour to reduce the design complexity and to enable modular reasoning about both aspects independently as well as in combination. By an example, we show how to use this framework in order to verify properties of synchronous adaptive systems. Modular reasoning in combination with abstraction mechanisms makes automatic model checking efficiently applicable.
Full Text
BibTeX
@InProceedings{ Schaefer.Poetzsch-Heffter06.abstraction,
title = { Using Abstraction in Modular Verification of Synchronous Adaptive Systems },
author = { Ina Schaefer and Arnd Poetzsch-Heffter },
booktitle = { Proceedings of "Workshop on Trustworthy Software", Saarbrücken, May 18-19, 2006 },
publisher = { Dagstuhl Online Proceedings },
note = { available at http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=699 },
month = may,
year = 2006,
}
This publication belongs to the project
EVAS.
