Hierarchical Modeling and Formal Verification: An Industrial Case Study Using Reo and Vereofy

Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz, Andries StamAndries Stam, Christel BaierChristel Baier

DOI Link

Joachim Klein, Sascha Klüppelholz, Andries Stam, Christel Baier
Hierarchical Modeling and Formal Verification: An Industrial Case Study Using Reo and Vereofy
Proc. of the 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), volume 6959 of Lecture Notes in Computer Science, 228--243, 2011. Springer

Details
Bibtex

KurzfassungAbstract
In traditional approaches to software development, modeling precedes programming activities. Hence, models represent the intended structure and behavior of the system-to-be. The reverse case, however, is often found in practice: using models to gain insight into an existing software system, enabling the evolution and refactoring of the system to new needs. We report on a case study with the ASK communication platform, an existing distributed software system with multithreaded components. For the modeling of the ASK system we followed a hierarchical top-down approach that allows a high-level description of the system behavior on different levels of abstraction by applying an iterative refinement procedure. The system model is refined by decomposing the components into sub-components together with the “glue code” that orchestrates their interactions. Our model of the ASK system is based on the exogenous coordination language Reo for specifying the glue code and an automata-based formalism for specifying the component interfaces. This approach is supported by the modeling framework of the tool-set Vereofy which is used to establish several properties of the components and the coordination mechanism of the ASK system. Besides demonstrating how modeling and verification can be used in combination to gain insight into legacy software, this case study also illustrates the applicability of exogenous coordination languages such as Reo for modeling and tool-sets such as Vereofy for the formal analysis of industrial systems.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-24431-5_17.

@inproceedings{KKSB2011,
  author    = {Joachim Klein and Sascha Kl{\"{u}}ppelholz and Andries Stam and
               Christel Baier},
  title     = {Hierarchical Modeling and Formal Verification: An Industrial Case
               Study Using Reo and Vereofy},
  booktitle = {Proc. of the 16th International Workshop on Formal Methods for
               Industrial Critical Systems (FMICS)},
  series    = {Lecture Notes in Computer Science},
  volume    = {6959},
  publisher = {Springer},
  year      = {2011},
  pages     = {228--243},
  doi       = {10.1007/978-3-642-24431-5_17}
}