Trustworthy Systems

Preface: Proceedings of the workshop on models for formal analysis of real systems

Authors

Rob van Glabbeek, Jan Friso Groote and Peter Hoefner

NICTA

UNSW

Eindhoven University of Technology

Abstract

This volume contains the proceedings of MARS 2015, the first workshop on Models for Formal Analysis of Real Systems, held on November 23, 2015 in Suva, Fiji, as an affiliated workshop of LPAR 2015, the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. The workshop emphasises modelling over verification. It aims at discussing the lessons learned from making formal methods for the verification and analysis of realistic systems. Examples are: (1) Which formalism is chosen, and why? (2) Which abstractions have to be made and why? (3) How are important characteristics of the system modelled? (4) Were there any complications while modelling the system? (5) Which measures were taken to guarantee the accuracy of the model?

We invited papers that present full models of real systems, which may lay the basis for future comparison and analysis. An aim of the workshop is to present different modelling approaches and discuss pros and cons for each of them. Alternative formal descriptions of the systems presented at this workshop are encouraged, which should foster the development of improved specification formalisms.

BibTeX Entry

  @inbook{vanGlabbeek_GH_15,
    author           = {van Glabbeek, Robert and Groote, Jan Friso and H\"ofner, Peter},
    booktitle        = {Electronic Proceedings in Theoretical Computer Science},
    editor           = {{Robert J. van Glabbeek, Jan Friso Groote and Peter H\"ofner}},
    issn             = {2075-2180},
    month            = nov,
    pages            = {-},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9088.pdf},
    publisher        = {Open Publishing Association},
    title            = {Preface: {P}roceedings of the Workshop on Models for Formal Analysis of Real Systems},
    volume           = {196},
    year             = {2015}
  }

Download