Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems
This work is incremental, as it builds on previous workshops to provide a platform for researchers to share formal models of real systems, addressing gaps in typical research publications.
The paper addresses the lack of detailed formal models for real systems in research by presenting proceedings from the MARS 2020 workshop, which focuses on developing and sharing accurate models from areas like networks and cyber-physical systems to demonstrate applicability beyond toy examples.
This volume contains the proceedings of MARS 2020, the fourth workshop on Models for Formal Analysis of Real Systems held as part of ETAPS 2020, the European Joint Conferences on Theory and Practice of Software. The MARS workshop brings together researchers from different communities who are developing formal models of real systems in areas where complex models occur, such as networks, cyber-physical systems, hardware/software codesign, biology, etc. The MARS workshops stem from two observations: (1) Large case studies are essential to show that specification formalisms and modelling techniques are applicable to real systems, whereas many research papers only consider toy examples or tiny case studies. (2) Developing an accurate model of a real system takes a large amount of time, often months or years. In most scientific papers, however, salient details of the model need to be skipped due to lack of space, and to leave room for formal verification methodologies and results. The MARS workshop remedies these issues, emphasising modelling over verification, so as to retain lessons learnt from formal modelling, which are not usually discussed elsewhere.