Volume
OASIcs, Volume 3
Workshop on Trustworthy Software
- Part of: Series: Open Access Series in Informatics (OASIcs)
Publication Details
- published at: 2006-09-26
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-02-6
- DBLP: db/conf/dagstuhl/P6000
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 3, Trustworthy SW'06, Complete Volume
Abstract
OASIcs, Volume 3, Trustworthy SW'06, Complete Volume
Cite as
Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@Proceedings{autexier_et_al:OASIcs.TrustworthySW.2006,
title = {{OASIcs, Volume 3, Trustworthy SW'06, Complete Volume}},
booktitle = {Workshop on Trustworthy Software},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-02-6},
ISSN = {2190-6807},
year = {2012},
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},
URN = {urn:nbn:de:0030-drops-35659},
doi = {10.4230/OASIcs.TrustworthySW.2006},
annote = {Keywords: Software/Program Verification}
}
Document
Front Matter
Preface -- Workshop Trustworthy Software 2006
Abstract
As part of the Interreg III C/E-Bird project "Recherches sans
fronti\`eres/Forschen ohne Grenzen" the Saarland University
organized a two-day workshop about "Trustworthy Software" in order
to present and foster the research competence in the
SaarLorLuxWallonie region in the area of developing safe, secure and
reliable software, computers and networks. The workshop especially
provided a forum for young scientists to present their research to a
transnational audience from the SaarLorLuxWallonie region and
consisted of 21 regular presentations and one invited presentation.
Cite as
Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. i-vi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{autexier_et_al:OASIcs.TrustworthySW.2006.693,
author = {Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
title = {{Preface -- Workshop Trustworthy Software 2006}},
booktitle = {Workshop on Trustworthy Software},
pages = {i--vi},
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.693},
URN = {urn:nbn:de:0030-drops-6932},
doi = {10.4230/OASIcs.TrustworthySW.2006.693},
annote = {Keywords: Trustworthy software, preface}
}
Document
Abstracts Collection -- Workshop Trustworthy Software 2006
Abstract
On 18-19 May 2006, the Saarland University organized a two-day
workshop about "Trustworthy Software" in order to present and foster
the research competence in the SaarLorLuxWallonie region in the area
of developing safe, secure and reliable software, computers and
networks. As part of the Interreg III C E-Bird project "Recherches
sans fronti\`eres/Forschen ohne Grenzen" it provided an excellent forum
especially for young scientists to present and discuss recent results,
new ideas and future research directions to a transnational audience
from the SaarLorLuxWallonie region. The workshop consisted of 21
regular presentations and one invited talk. Abstracts of all
presentations are collected in this paper, including links to extended
abstracts or full papers. The first section directs to the preface of
the proceedings.
Cite as
Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper. Abstracts Collection -- Workshop Trustworthy Software 2006. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{autexier_et_al:OASIcs.TrustworthySW.2006.758,
author = {Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
title = {{Abstracts Collection -- Workshop Trustworthy Software 2006}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--7},
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.758},
URN = {urn:nbn:de:0030-drops-7588},
doi = {10.4230/OASIcs.TrustworthySW.2006.758},
annote = {Keywords: Software evolution, Modularity, Automated debugging, Dependability assurance, Failure analysis, Static program analysis, Infinite and Finite-state verification, Runtime verification, Theorem proving, Access control, Security analysis, Security protocols, E-Voting}
}
Document
An Introduction to the Tool Ticc
Abstract
This paper is a tutorial introduction to the sociable interface model
of [12] and its underlying tool \textsc{Tcc}. The
paper starts with a survey of the theory of interfaces and then
introduces the sociable interface model that is a game-based model
with rich communication primitives to facilitate the modeling of
software and distributed systems. The model and its
main features are then intensivelly discussed and illustrated using
the tool \textsc{Tcc}.
Cite as
Axel Legay, Luca de Alfaro, and Marco Faella. An Introduction to the Tool Ticc. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{legay_et_al:OASIcs.TrustworthySW.2006.766,
author = {Legay, Axel and de Alfaro, Luca and Faella, Marco},
title = {{An Introduction to the Tool Ticc}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--32},
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.766},
URN = {urn:nbn:de:0030-drops-7667},
doi = {10.4230/OASIcs.TrustworthySW.2006.766},
annote = {Keywords: Open system, game, interface automata}
}
Document
An Operator-based Approach to Incremental Development of Conform Protocol State Machines
Abstract
An incremental development framework which supports a conform construction of Protocol State Machines (PSMs) is presented. We capture design concepts and strategies of PSM construction by sequentially applying some development operators: each operator makes evolve the current PSM to another one. To ensure a conform construction, we introduce three conformance relations, inspired by the specification refinement and specification matchings supported by formal methods. Conformance relations preserve some global behavioral properties. Our purpose is illustrated by some development steps of the card service interface of an electronic purse: for each step, we introduce the idea of the development, we propose an operator and we give the new specification state obtained by the application of this operator and the property of this state relatively to the previous one in terms of conformance relation.
Cite as
Arnaud Lanoix, Dieu-Donné Okalas Ossami, and Jeanine Souquières. An Operator-based Approach to Incremental Development of Conform Protocol State Machines. 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{lanoix_et_al:OASIcs.TrustworthySW.2006.695,
author = {Lanoix, Arnaud and Okalas Ossami, Dieu-Donn\'{e} and Souqui\`{e}res, Jeanine},
title = {{An Operator-based Approach to Incremental Development of Conform Protocol State Machines}},
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.695},
URN = {urn:nbn:de:0030-drops-6953},
doi = {10.4230/OASIcs.TrustworthySW.2006.695},
annote = {Keywords: Protocol state machine, incremental development, development operator, exact conformance, plugin conformance, partial conformance}
}
Document
Explaining Data Type Reduction in the Shape Analysis Framework
Abstract
Automatic formal verification of systems composed of a large or even unbounded
number of components is difficult as the state space of these systems is
prohibitively large. Abstraction techniques automatically construct finite
approximations of infinite-state systems from which safe information about
the original system can be inferred. We study two abstraction techniques
shape analysis, a technique from program analysis, and data type reduction,
originating from model checking. Until recently we did not properly understand
how shape analysis and data type reduction relate. In this talk, we shed light
on this relation in a comprehensive way. This is a step towards a more
unified view of abstraction employed in the static analysis and model checking
community.
Cite as
Björn Wachter. Explaining Data Type Reduction in the Shape Analysis Framework. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{wachter:OASIcs.TrustworthySW.2006.701,
author = {Wachter, Bj\"{o}rn},
title = {{Explaining Data Type Reduction in the Shape Analysis Framework}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--6},
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.701},
URN = {urn:nbn:de:0030-drops-7016},
doi = {10.4230/OASIcs.TrustworthySW.2006.701},
annote = {Keywords: Canonical abstraction, data type reduction, model checking, parameterized system, infinite-state}
}
Document
Formal Validation of Pattern Matching code
Abstract
When addressing the formal validation of generated software, two main
alternatives consist either to prove the correctness of compilers or
to directly validate the generated code. Here, we focus on directly
proving the correctness of compiled code issued from powerful
pattern matching constructions typical of ML like languages or
rewrite based languages such as ELAN, MAUDE or Tom.
In this context, our first contribution is to define a general
framework for anchoring algebraic pattern-matching capabilities
in existing languages like C, Java or ML. Then, using a just enough
powerful intermediate language, we formalize the behavior of compiled
code and define the correctness of compiled code with respect to
pattern-matching behavior. This allows us to prove the equivalence of
compiled code correctness with a generic first-order proposition whose
proof could be achieved via a proof assistant or an automated theorem
prover. We then extend these results to the multi-match situation
characteristic of the ML like languages.
The whole approach has been implemented on top of the Tom compiler
and used to validate the syntactic matching code of the Tom compiler
itself.
Cite as
Claude Kirchner, Pierre-Etienne Moreau, and Antoine Reilles. Formal Validation of Pattern Matching code. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{kirchner_et_al:OASIcs.TrustworthySW.2006.697,
author = {Kirchner, Claude and Moreau, Pierre-Etienne and Reilles, Antoine},
title = {{Formal Validation of Pattern Matching code}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--22},
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.697},
URN = {urn:nbn:de:0030-drops-6978},
doi = {10.4230/OASIcs.TrustworthySW.2006.697},
annote = {Keywords: Correctness proofs, compilers, pattern matching, validation}
}
Document
Formalizing On Chip Communications in a Functional Style
Abstract
This paper presents a formal model for representing {it any} on-chip communication architecture.
This model is described mathematically by a function, named $mathit{GeNoC}$.
The correctness of $mathit{GeNoC}$ is expressed as a theorem, which states that messages emitted
on the architecture reach their expected destination without modification of their content.
The model identifies the key constituents common to {it all} communication architectures and their essential properties,
from which the proof of the $GeNoC$ theorem is deduced.
Each constituent is represented by a function which has no {it explicit} definition but is constrained
to satisfy the essential properties.
Thus, the validation of a {it particular} architecture is reduced to the proof that its concrete definition satisfies the essential properties.
In practice, the model has been defined in the logic of the ACL2 theorem proving system.
We define a methodology that yields a systematic approach to the validation of communication architectures
at a high level of abstraction. To validate our approach, we exhibit several architectures that constitute
concrete instances of the generic model $GeNoC$. Some of these applications come from industrial designs, such as
the AMBA AHB bus or the Octagon network from ST Microelectronics.
Cite as
Julien Schmaltz and Dominique Borrione. Formalizing On Chip Communications in a Functional Style. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{schmaltz_et_al:OASIcs.TrustworthySW.2006.700,
author = {Schmaltz, Julien and Borrione, Dominique},
title = {{Formalizing On Chip Communications in a Functional Style}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--25},
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.700},
URN = {urn:nbn:de:0030-drops-7000},
doi = {10.4230/OASIcs.TrustworthySW.2006.700},
annote = {Keywords: SoC's, communication architectures, formal methods, automated theorem proving}
}
Document
Isolating Intrusions by Automatic Experiments
Abstract
When dealing with malware infections, one of the first tasks is to find the processes that were involved in the attack. We introduce Malfor, a system that isolates those processes automatically. In contrast to other methods that help analyze attacks, Malfor works by experiments: first, we record the interaction of the system under attack; after the intrusion has been detected, we replay the recorded events in slightly different configurations to see which processes were relevant for the intrusion. This approach has three advantages over deductive approaches: first, the processes that are thus found have been experimentally shown to be relevant for the attack; second, the amount of evidence that must then be analyzed to find the attack vector is greatly reduced; and third, Malfor itself cannot make wrong deductions. In a first experiment, Malfor was able to extract the three processes responsible for an attack from 32 candidates in about six minutes.
Cite as
Stephan Neuhaus. Isolating Intrusions by Automatic Experiments. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{neuhaus:OASIcs.TrustworthySW.2006.696,
author = {Neuhaus, Stephan},
title = {{Isolating Intrusions by Automatic Experiments}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--3},
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.696},
URN = {urn:nbn:de:0030-drops-6960},
doi = {10.4230/OASIcs.TrustworthySW.2006.696},
annote = {Keywords: Intrusion Analysis, Malware, Experimentation}
}
Document
Relating two standard notions of secrecy
Abstract
Two styles of definitions are usually considered to
express that a security protocol preserves the confidentiality of a
data { t s}. Reach-ability-based secrecy means that { t s} should
never be disclosed while equi-valence-based secrecy states that two
executions of a protocol with distinct instances for { t s} should
be indistinguishable to an attacker. Although the second formulation
ensures a higher level of security and is closer to cryptographic
notions of secrecy, decidability results and automatic tools have
mainly focused on the first definition so far.
This paper initiates a systematic investigation of situations where
syntactic secrecy entails strong secrecy.
We show that in the passive case, reachability-based secrecy
actually implies equivalence-based secrecy for signatures, symmetric
and asymmetric encryption provided that the primitives are
probabilistic. For active adversaries in the case of symmetric
encryption, we provide sufficient (and rather tight) conditions on
the protocol for this implication to hold.
Cite as
Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch. Relating two standard notions of secrecy. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{zalinescu_et_al:OASIcs.TrustworthySW.2006.691,
author = {Zalinescu, Eugen and Cortier, V\'{e}ronique and Rusinowitch, Micha\"{e}l},
title = {{Relating two standard notions of secrecy}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--29},
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.691},
URN = {urn:nbn:de:0030-drops-6911},
doi = {10.4230/OASIcs.TrustworthySW.2006.691},
annote = {Keywords: Verification, security protocols, secrecy, applied-pi calculus}
}
Document
SANA - Security Analysis in Internet Traffic through Artificial Immune Systems
Abstract
The Attacks done by Viruses, Worms, Hackers, etc. are a Network Security-Problem in many Organisations. Current Intrusion Detection Systems have significant Disadvantages, e.g. the need of plenty of Computational Power or the Local Installation. Therefore, we introduce a novel Framework for Network Security which is called SANA. SANA contains an artificial Immune System with artificial Cells which perform certain Tasks in order to to support existing systems to better secure the Network against Intrusions. The Advantages of SANA are that it is efficient, adaptive, autonomous, and massively-distributed. In this Article, we describe the Architecture of the artificial Immune System and the Functionality of the Components. We explain briefly the Implementation and discuss Results.
Cite as
Michael Hilker and Christoph Schommer. SANA - Security Analysis in Internet Traffic through Artificial Immune Systems. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{hilker_et_al:OASIcs.TrustworthySW.2006.694,
author = {Hilker, Michael and Schommer, Christoph},
title = {{SANA - Security Analysis in Internet Traffic through Artificial Immune Systems}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--9},
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.694},
URN = {urn:nbn:de:0030-drops-6949},
doi = {10.4230/OASIcs.TrustworthySW.2006.694},
annote = {Keywords: Artificial Immune Systems, Network Security, Intrusion Detection, Artificial Cell Communication, Biological-Inspired Computing, Complex Adaptive Syste}
}
Document
Shape Analysis of Sets
Abstract
Shape Analysis is concerned with determining "shape invariants", i.e. structural properties of the heap, for programs that manipulate pointers and heap-allocated storage. Recently, very precise shape analysis algorithms have been developed that are able to prove the partial correctness of heap-manipulating programs. We explore the use of shape analysis to analyze abstract data types (ADTs). The ADT Set shall serve as an example, as it is widely used and can be found in most of the major data type libraries, like STL, the Java API, or LEDA. We formalize our notion of the ADT Set by algebraic specification. Two prototypical C set implementations are presented, one based on lists, the other on trees. We instantiate a parametric shape analysis framework to generate analyses that are able to prove the compliance of the two implementations to their specification.
Cite as
Jan Reineke. Shape Analysis of Sets. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
Copy BibTex To Clipboard
@InProceedings{reineke:OASIcs.TrustworthySW.2006.698,
author = {Reineke, Jan},
title = {{Shape Analysis of Sets}},
booktitle = {Workshop on Trustworthy Software},
pages = {1--19},
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.698},
URN = {urn:nbn:de:0030-drops-6980},
doi = {10.4230/OASIcs.TrustworthySW.2006.698},
annote = {Keywords: Shape analysis, adt, algebraic specification, invariants, verification, set implementations, imperative programs}
}
Document
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.
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}
}