Design and Verification of Systems with Exogenous Coordination Using Vereofy

Christel BaierChristel Baier, Tobias BlechmannTobias Blechmann, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz, Wolfgang LeisterWolfgang Leister

DOI Link

Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Klüppelholz, Wolfgang Leister
Design and Verification of Systems with Exogenous Coordination Using Vereofy
Proc. of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 6416 of Lecture Notes in Computer Science, 97--111, 2010. Springer

Details
Bibtex

KurzfassungAbstract
The feasibility of formal methods for the analysis of complex systems crucially depends on a modeling framework that supports compositional design, stepwise refinement and abstractions. An important feature is the clear separation of coordination and computation which permits to apply various verification techniques for the computation performed by components and interactions as well as dependencies between the components. We report here on a model-checking approach using the tool Vereofy that is based on an exogenous coordination model, where the components are represented by their behavioral interfaces. Vereofy supports the verification of the components and their communication structure. Our approach is illustrated by means of a case study with a sensor network where Vereofy has been used to establish several properties of the sensor nodes and their routing procedures.
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-16561-0_15.

@inproceedings{BBKKL2010,
  author    = {Christel Baier and Tobias Blechmann and Joachim Klein and Sascha
               Kl{\"{u}}ppelholz and Wolfgang Leister},
  title     = {Design and Verification of Systems with Exogenous Coordination
               Using Vereofy},
  booktitle = {Proc. of the 4th International Symposium On Leveraging
               Applications of Formal Methods, Verification and Validation
               (ISoLA)},
  series    = {Lecture Notes in Computer Science},
  volume    = {6416},
  publisher = {Springer},
  year      = {2010},
  pages     = {97--111},
  doi       = {10.1007/978-3-642-16561-0_15}
}