License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.TrustworthySW.2006.699
URN: urn:nbn:de:0030-drops-6996
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/699/
Go to the corresponding OASIcs Volume Portal

Schaefer, Ina ; Poetzsch-Heffter, Arnd

Using Abstraction in Modular Verification of Synchronous Adaptive Systems

pdf-format:
06000.SchaeferIna.Paper.699.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{schaefer_et_al:OASIcs:2006:699,
  author =	{Ina Schaefer and Arnd Poetzsch-Heffter},
  title =	{{Using Abstraction in Modular Verification of Synchronous Adaptive Systems}},
  booktitle =	{Workshop on Trustworthy Software},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Serge Autexier and Stephan Merz and Leon van der Torre and Reinhard Wilhelm and Pierre Wolper},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2006/699},
  URN =		{urn:nbn:de:0030-drops-6996},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.699},
  annote =	{Keywords: Dependable Embedded Systems, Self-Adaptation, Abstraction, Modular Verification}
}

Keywords: Dependable Embedded Systems, Self-Adaptation, Abstraction, Modular Verification
Collection: Workshop on Trustworthy Software
Issue Date: 2006
Date of publication: 26.09.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI