1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)

Document

Complete Volume

DOI: 10.4230/OASIcs.FSFMA.2013

OASIcs, Volume 31, FSFMA'13, Complete Volume

Authors: Christine Choppy and Jun Sun

Abstract

OASIcs, Volume 31, FSFMA'13, Complete Volume

Cite as

1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{choppy_et_al:OASIcs.FSFMA.2013,
  title =	{{OASIcs, Volume 31, FSFMA'13, Complete Volume}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013},
  URN =		{urn:nbn:de:0030-drops-41281},
  doi =		{10.4230/OASIcs.FSFMA.2013},
  annote =	{Keywords: Formal methods}
}

Document

Front Matter

DOI: 10.4230/OASIcs.FSFMA.2013.i

Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Christine Choppy and Jun Sun

Abstract

Frontmatter, Table of Contents, Preface, Workshop Organization

Cite as

1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. i-xiii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{choppy_et_al:OASIcs.FSFMA.2013.i,
  author =	{Choppy, Christine and Sun, Jun},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{i--xiii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.i},
  URN =		{urn:nbn:de:0030-drops-40819},
  doi =		{10.4230/OASIcs.FSFMA.2013.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}

Document

Invited Talk

DOI: 10.4230/OASIcs.FSFMA.2013.1

Control of Switching Systems by Invariance Analysis (Invited Talk)

Authors: Laurent Fribourg

Abstract

Switched systems are embedded devices widespread in industrial applications such as power electronics and automotive control. They consist of continuous-time dynamical subsystems and a rule that controls the switching between them. Under a suitable control rule, the system can improve its steady-state performance and meet essential properties such as safety and stability in desirable operating zones. We explain that such controller synthesis problems are related to the construction of appropriate invariants of the state space, which approximate the limit sets of the system trajectories. We present a new approach of invariant construction based on a technique of state space decomposition interleaved with forward fixed point computation. The method is illustrated in a case study taken from the field of power electronics.

Cite as

Laurent Fribourg. Control of Switching Systems by Invariance Analysis (Invited Talk). In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fribourg:OASIcs.FSFMA.2013.1,
  author =	{Fribourg, Laurent},
  title =	{{Control of Switching Systems by Invariance Analysis}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{1--1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.1},
  URN =		{urn:nbn:de:0030-drops-40836},
  doi =		{10.4230/OASIcs.FSFMA.2013.1},
  annote =	{Keywords: Control theory, Hybrid systems, Safety, Stability}
}

Document

Invited Talk

DOI: 10.4230/OASIcs.FSFMA.2013.2

Specification, Verification and Inference (Invited Talk)

Authors: Wei-Ngan Chin

Abstract

Traditionally, the focus of specification mechanism has been on improving its ability to cover a wider range of problems more accurately, while the effectiveness of verification is left to the underlying theorem provers. Our work attempts a novel approach, where the focus is on designing good specification mechanisms that can achieve both better expressiveness and better verifiability. Moreover, we shall also highlight a unified specification mechanism that can be used for both verification and inference. Our framework allows preconditions and postconditions to be selectively inferred via a set of uninterpreted relations which are computed using bi-abduction, and modularly synthesized to support concise specification for program codes.

Cite as

Wei-Ngan Chin. Specification, Verification and Inference (Invited Talk). In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, p. 2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{chin:OASIcs.FSFMA.2013.2,
  author =	{Chin, Wei-Ngan},
  title =	{{Specification, Verification and Inference}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{2--2},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.2},
  URN =		{urn:nbn:de:0030-drops-40827},
  doi =		{10.4230/OASIcs.FSFMA.2013.2},
  annote =	{Keywords: Expressive Specification, Automated Verification, Specification Inference}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.3

Analysis of Two-Layer Protocols: DCCP Simultaneous-Open and Hole Punching Procedures

Authors: Somsak Vanit-Anunchai

Abstract

The simultaneous-open procedure of the Datagram Congestion Control Protocol (DCCP), RFC 5596, was published in September 2009. Its design aims to overcome DCCP weaknesses when the Server is behind a middle box, such as Network Address Translators or firewalls. The original DCCP specification, RFC 4340, only allows the Client to initiate the call. The call request cannot reach the Server behind the middle box. A widely used solution to address this problem is called the hole punching technique. This technique requires the Server to initiate sending packets. Using Coloured Petri Nets (CPN) this paper models and analyses the DCCP procedure specified in RFC 5596. However, the difficulty is that detailed modelling of the address translation is also required. This causes state space explosion. We alleviate the state explosion using prioritized transitions and the sweep-line technique. Modelling and analysis approaches are discussed in the hope that it is helpful for others who wish to analyse similar protocols. Analysis results are also obtained for the simultaneous-open procedure specified in RFC 5596.

Cite as

Somsak Vanit-Anunchai. Analysis of Two-Layer Protocols: DCCP Simultaneous-Open and Hole Punching Procedures. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 3-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{vanitanunchai:OASIcs.FSFMA.2013.3,
  author =	{Vanit-Anunchai, Somsak},
  title =	{{Analysis of Two-Layer Protocols: DCCP Simultaneous-Open and Hole Punching Procedures}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{3--17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.3},
  URN =		{urn:nbn:de:0030-drops-40846},
  doi =		{10.4230/OASIcs.FSFMA.2013.3},
  annote =	{Keywords: Network Address Translators, Coloured Petri Nets, Sweep-line Method, Prioritized Transitions}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.18

Dynamic Clock Elimination in Parametric Timed Automata

Authors: Étienne André

Abstract

The formalism of parametric timed automata provides designers with a formal way to specify and verify real-time concurrent systems where iming requirements are unknown (or parameters). Such models are usually subject to the state space explosion. A popular way to partially reduce the size of the state space is to reduce the number of clock variables. In this work, we present a technique for dynamically eliminating clocks. Experiments using IMITATOR show a diminution of the number of states and of the computation time, and in some cases allow termination of the analysis of models that could not terminate otherwise. More surprisingly, even when the number of clocks remains constant, there is little noticeable overhead in applying the proposed clock elimination.

Cite as

Étienne André. Dynamic Clock Elimination in Parametric Timed Automata. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 18-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{andre:OASIcs.FSFMA.2013.18,
  author =	{Andr\'{e}, \'{E}tienne},
  title =	{{Dynamic Clock Elimination in Parametric Timed Automata}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{18--31},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.18},
  URN =		{urn:nbn:de:0030-drops-40855},
  doi =		{10.4230/OASIcs.FSFMA.2013.18},
  annote =	{Keywords: Verification, Real-time systems, Parameter synthesis, State space reduction, Inverse Method}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.32

On the Determinism of Multi-core Processors

Authors: Vladimir-Alexandru Paun, Bruno Monsuez, and Philippe Baufreton

Abstract

Hard real time systems are evolving in order to respond to the increasing demand in complex functionalities while taking advantage of newer hardware. Software development for safety critical systems has to comply with strict requirements that will facilitate the certification process. During this process, each part of the system is evaluated, requiring a certain level of assurance in order to provide confidence in the product. In particular there must be a level of confidence that the system behaves deterministically that may be based on functionality, resources and time. The success of system verification depends greatly on the capacity to determine its exact behavior. Nonetheless, hardware evolved in order to maximize the average computation power throughput with little to no regard to the deterministic aspect. Therefore modern architectural features of processors, like pipelines, cache memories and co-processors, make it hard to verify that all the needed properties are respected. The multi-core is furthermore difficult to analyze as the architecture employs mechanisms that compromise strong spatial and temporal partitioning when using shared resources without rigorous access control like shared caches or shared input/outputs. In this paper we identify and analyze the main sources of nondeterminism of the multi-cores with regard to the timing estimation. Precise determination of the worst case execution time is a challenging task even in single-core architectures. The problems are accentuated in the multi-core context mainly due to the resource sharing that can lead to highly complex interactions or to nondeterminism. Most of the units that generate behaviors that are hard to take into account can be deactivated, but it is not always easy to predict the impact on the performance. Nevertheless some of the features cannot be disabled (such as the out of order execution or some nondeterministic crossbar access policies) which leads to the invalidation of the respective platform for applications with high criticality level. We will address the problematic units, propose configuration or architecture guidelines and estimate their impact on the performance and determinism of the system.

Cite as

Vladimir-Alexandru Paun, Bruno Monsuez, and Philippe Baufreton. On the Determinism of Multi-core Processors. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 32-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{paun_et_al:OASIcs.FSFMA.2013.32,
  author =	{Paun, Vladimir-Alexandru and Monsuez, Bruno and Baufreton, Philippe},
  title =	{{On the Determinism of Multi-core Processors}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{32--46},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.32},
  URN =		{urn:nbn:de:0030-drops-40869},
  doi =		{10.4230/OASIcs.FSFMA.2013.32},
  annote =	{Keywords: multi-core, determinism, hard-real time systems}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.47

An Improved Construction of Petri Net Unfoldings

Authors: César Rodríguez and Stefan Schwoon

Abstract

Petri nets are a well-known model language for concurrent systems. The unfolding of a Petri net is an acyclic net bisimilar to the original one. Because it is acyclic, it admits simpler decision problems though it is in general larger than the net. In this paper, we revisit the problem of efficiently constructing an unfolding. We propose a new method that avoids computing the concurrency relation and therefore uses less memory than some other methods but still represents a good time-space tradeoff. We implemented the approach and report on experiments.

Cite as

César Rodríguez and Stefan Schwoon. An Improved Construction of Petri Net Unfoldings. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 47-52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{rodriguez_et_al:OASIcs.FSFMA.2013.47,
  author =	{Rodr{\'\i}guez, C\'{e}sar and Schwoon, Stefan},
  title =	{{An Improved Construction of Petri Net Unfoldings}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{47--52},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.47},
  URN =		{urn:nbn:de:0030-drops-40875},
  doi =		{10.4230/OASIcs.FSFMA.2013.47},
  annote =	{Keywords: Concurrency, Petri nets, partial orders, unfoldings}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.53

Constructing Attractors of Nonlinear Dynamical Systems

Authors: Laurent Fribourg, Ulrich Kühne, and Romain Soulat

Abstract

In a previous work, we have shown how to generate attractor sets of affine hybrid systems using a method of state space decomposition. We show here how to adapt the method to polynomial dynamics systems by approximating them as switched affine systems. We show the practical interest of the method on standard examples of the literature.

Cite as

Laurent Fribourg, Ulrich Kühne, and Romain Soulat. Constructing Attractors of Nonlinear Dynamical Systems. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 53-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fribourg_et_al:OASIcs.FSFMA.2013.53,
  author =	{Fribourg, Laurent and K\"{u}hne, Ulrich and Soulat, Romain},
  title =	{{Constructing Attractors of Nonlinear Dynamical Systems}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{53--60},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.53},
  URN =		{urn:nbn:de:0030-drops-40885},
  doi =		{10.4230/OASIcs.FSFMA.2013.53},
  annote =	{Keywords: Control theory, Hybrid Systems, Nonlinear dynamical systems}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.61

Formal Modelling and Verification of Pervasive Computing Systems

Authors: Yan Liu

Abstract

Pervasive computing (PvC) systems are emerging as promising solutions to many practical problems, e.g., elderly care in home. However, such systems have long been developed without sufficient verification. Formal methods, eps. model checking are sound techniques for complex system analysis regarding correctness and reliability requirements. In this work, a formal modelling framework is proposed to model the general the system design (e.g., concurrent communications) and the critical environment inputs (e.g., human behaviours). Correctness requirements are specified in formal logics which are automatically verifiable against a system model. Furthermore, Markov Decision Processes (MDPs) are adopted for modelling probabilistic behaviours of PvC systems. Three problems are analysed which are overall reliability prediction based on component reliabilities, reliability distribution w.r.t., how reliable should the component be to reach an overall reliability requirement and sensitivity analysis w.r.t., how does a component reliability affect the overall reliability. Finally, the usefulness of our approaches are demonstrated on a smart healthcare system with unexpected bugs and system flaws exposed.

Cite as

Yan Liu. Formal Modelling and Verification of Pervasive Computing Systems. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 61-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{liu:OASIcs.FSFMA.2013.61,
  author =	{Liu, Yan},
  title =	{{Formal Modelling and Verification of Pervasive Computing Systems}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{61--67},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.61},
  URN =		{urn:nbn:de:0030-drops-40892},
  doi =		{10.4230/OASIcs.FSFMA.2013.61},
  annote =	{Keywords: System Analysis, Formal Modelling and Verification, Reliability Analysis}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.68

Illustrating the Mezzo programming language

Authors: Jonathan Protzenko

Abstract

When programmers want to prove strong program invariants, they are usually faced with a choice between using theorem provers and using traditional programming languages. The former requires them to provide program proofs, which, for many applications, is considered a heavy burden. The latter provides less guarantees and the programmer usually has to write run-time assertions to compensate for the lack of suitable invariants expressible in the type system. We introduce Mezzo, a programming language in the tradition of ML, in which the usual concept of a type is replaced by a more precise notion of a permission. Programs written in Mezzo usually enjoy stronger guarantees than programs written in pure ML. However, because Mezzo is based on a type system, the reasoning requires no user input. In this paper, we illustrate the key concepts of Mezzo, highlighting the static guarantees our language provides.

Cite as

Jonathan Protzenko. Illustrating the Mezzo programming language. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 68-73, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{protzenko:OASIcs.FSFMA.2013.68,
  author =	{Protzenko, Jonathan},
  title =	{{Illustrating the Mezzo programming language}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{68--73},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.68},
  URN =		{urn:nbn:de:0030-drops-40905},
  doi =		{10.4230/OASIcs.FSFMA.2013.68},
  annote =	{Keywords: Type system, Language design, ML, Permissions}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.74

Improving System-Level Verification of SystemC Models with SPIN

Authors: Martin Elshuber, Susanne Kandl, and Peter Puschner

Abstract

SystemC is a de-facto industry standard for developing, modelling, and simulating embedded systems. As embedded systems become more and more integrated into many aspects of human lives (e.g., transportation, surveillance systems, ...), failures of embedded systems might cause dangerous hazards to individuals or groups. Guaranteeing safety of such systems makes formal verification crucial. In this paper we present a novel approach for verifying SystemC models with SPIN. Focusing on system-level verification we reuse compiled and executable code from the original model and embed it into the verifier generated by SPIN. In contrast to most other approaches, which require a complete model transformation, in our approach the transformation focuses only on the relevant parts of the model while leaving functional blocks untransformed. Our technique aims at reducing the state vector size managed by the verifier of SPIN, at improving state exploration performance by avoiding unnecessary model transformation steps, and at concentrating on verifying properties that emerge from the composition of multiple functional units.

Cite as

Martin Elshuber, Susanne Kandl, and Peter Puschner. Improving System-Level Verification of SystemC Models with SPIN. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 74-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{elshuber_et_al:OASIcs.FSFMA.2013.74,
  author =	{Elshuber, Martin and Kandl, Susanne and Puschner, Peter},
  title =	{{Improving System-Level Verification of SystemC Models with SPIN}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{74--79},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.74},
  URN =		{urn:nbn:de:0030-drops-40915},
  doi =		{10.4230/OASIcs.FSFMA.2013.74},
  annote =	{Keywords: SystemC, SPIN, Promela, System-Level Verification}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.80

Modelling and Reasoning about Dynamic Networks as Concurrent Systems

Authors: Yanti Rusmawati and David Rydeheard

Abstract

We propose a new approach to modelling and reasoning about dynamic networks. Dynamic networks consist of nodes and edges whose operating status may change over time (for example, the edges may be unreliable and operate intermittently). Message-passing in such networks is inherently difficult and reasoning about the behaviour of message-passing algorithms is also difficult. We develop a series of abstract models which allow us to focus on the correctness of routing methods. We model the dynamic network as a ``demonic'' process which runs concurrently with routing updates and message-passing. This allows us to use temporal logic and fairness constraints to reason about dynamic networks. The models are implemented as multi-threaded programs and, to validate them, we use an experimental run-time verification tool called RuleR.

Cite as

Yanti Rusmawati and David Rydeheard. Modelling and Reasoning about Dynamic Networks as Concurrent Systems. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 80-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{rusmawati_et_al:OASIcs.FSFMA.2013.80,
  author =	{Rusmawati, Yanti and Rydeheard, David},
  title =	{{Modelling and Reasoning about Dynamic Networks as Concurrent Systems}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{80--85},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.80},
  URN =		{urn:nbn:de:0030-drops-40921},
  doi =		{10.4230/OASIcs.FSFMA.2013.80},
  annote =	{Keywords: dynamic networks, temporal logic, concurrent systems}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.86

Safety of Unmanned Aircraft Systems Facing Multiple Breakdowns

Authors: Patrice Carle, Christine Choppy, Romain Kervarc, and Ariane Piel

Abstract

This work deals with data analysis issues in an aeronautics context by using a formal framework relying on activity recognition techniques which are applied to the certification and safety analysis processes of Unmanned Aircraft Systems in breakdown situations. In this paper, the behaviour of these systems is modelled, simulated and studied in case of multiple failures using a complex event processing language called chronicles to describe which combinations of events in time may lead to safety breaches, and a C++ chronicle recognition library is used to implement this method.

Cite as

Patrice Carle, Christine Choppy, Romain Kervarc, and Ariane Piel. Safety of Unmanned Aircraft Systems Facing Multiple Breakdowns. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 86-91, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{carle_et_al:OASIcs.FSFMA.2013.86,
  author =	{Carle, Patrice and Choppy, Christine and Kervarc, Romain and Piel, Ariane},
  title =	{{Safety of Unmanned Aircraft Systems Facing Multiple Breakdowns}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{86--91},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.86},
  URN =		{urn:nbn:de:0030-drops-40935},
  doi =		{10.4230/OASIcs.FSFMA.2013.86},
  annote =	{Keywords: complex event processing, safety, aeronautics, multiple breakdowns, behaviour recognition tool}
}

OASIcs, Volume 31

1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)

Event

Editors

Publication Details

Access Numbers

Documents

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Filters

Thanks for your feedback!

Could not send message