OASIcs, Volume 3

Workshop on Trustworthy Software



Thumbnail PDF

Event

TrustworthySW 2006, May 18-19, 2006, Saarbruecken, Germany

Editors

Serge Autexier
Stephan Merz
Leon van der Torre
Reinhard Wilhelm
Pierre Wolper

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

Documents

No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 3, Trustworthy SW'06, Complete Volume

Authors: Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper


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

Authors: Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper


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

Authors: Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper


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

Authors: Axel Legay, Luca de Alfaro, and Marco Faella


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

Authors: Arnaud Lanoix, Dieu-Donné Okalas Ossami, and Jeanine Souquières


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

Authors: Björn Wachter


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

Authors: Claude Kirchner, Pierre-Etienne Moreau, and Antoine Reilles


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

Authors: Julien Schmaltz and Dominique Borrione


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

Authors: Stephan Neuhaus


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

Authors: Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch


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

Authors: Michael Hilker and Christoph Schommer


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

Authors: Jan Reineke


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

Authors: Ina Schaefer and 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 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}
}

Filters


Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail