Using Abstraction in Modular Verification of Synchronous Adaptive Systems

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 fail- 
ures. 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 syn- 
chronous adaptive systems. The modelling separates functional and adap- 
tive 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 com- 
bination with abstraction mechanisms makes automatic model checking 
efficiently applicable.