DROPS

Document

Divide and Conquer: the Quest for Compositional Design and Analysis (Dagstuhl Seminar 12511)

Authors: Marieke Huismann, Barbara Jobstmann, Ina Schaefer, and Marielle Stoelinga

Published in: Dagstuhl Reports, Volume 2, Issue 12 (2013)

Abstract

On December 17 to 21, the Dagstuhl seminar "Divide and Conquer: the Quest for Compositional Design and Analysis" was organized. Topic was the compositionally, a central theme in computer science, but its applications, methods, techniques are scattered around many different disciplines. Therefore, this workshop brought together scientists from different disciplines, including deductive verification, model checking, software product lines, component interfaces.

Cite as

Marieke Huismann, Barbara Jobstmann, Ina Schaefer, and Marielle Stoelinga. Divide and Conquer: the Quest for Compositional Design and Analysis (Dagstuhl Seminar 12511). In Dagstuhl Reports, Volume 2, Issue 12, pp. 64-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{huismann_et_al:DagRep.2.12.64,
  author =	{Huismann, Marieke and Jobstmann, Barbara and Schaefer, Ina and Stoelinga, Marielle},
  title =	{{Divide and Conquer: the Quest for Compositional Design and Analysis (Dagstuhl Seminar 12511)}},
  pages =	{64--88},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{12},
  editor =	{Huismann, Marieke and Jobstmann, Barbara and Schaefer, Ina and Stoelinga, Marielle},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.12.64},
  URN =		{urn:nbn:de:0030-drops-39951},
  doi =		{10.4230/DagRep.2.12.64},
  annote =	{Keywords: Algorithms, Design, Languages, Theory, Verification}
}

Document

DOI: 10.4230/OASIcs.TrustworthySW.2006.699

Using Abstraction in Modular Verification of Synchronous Adaptive Systems

Authors: Ina Schaefer and Arnd Poetzsch-Heffter

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)

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.

Cite as

Ina Schaefer and Arnd Poetzsch-Heffter. Using Abstraction in Modular Verification of Synchronous Adaptive Systems. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{schaefer_et_al:OASIcs.TrustworthySW.2006.699,
  author =	{Schaefer, Ina and Poetzsch-Heffter, Arnd},
  title =	{{Using Abstraction in Modular Verification of Synchronous Adaptive Systems}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.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}
}

Search Results

Documents authored by Schaefer, Ina

Divide and Conquer: the Quest for Compositional Design and Analysis (Dagstuhl Seminar 12511)

Abstract

Cite as

Using Abstraction in Modular Verification of Synchronous Adaptive Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message