Proceedings Workshop on Models for Formal Analysis of Real Systems

TL;DR

This workshop proceedings discusses various modeling approaches for formal analysis of real systems, focusing on lessons learned, formalism choices, abstractions, and accuracy assurance in realistic system modeling.

Contribution

It presents diverse modeling approaches for real systems, fostering comparison and encouraging alternative formal descriptions to improve specification formalisms.

Findings

Different formal modeling techniques are evaluated.

Lessons learned from modeling real systems are shared.

Discussion on formalism choices and abstraction strategies.

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.