To show t hat a developed approach for automated reasoning a ctually scales to real systems, large case studies are essential. The development of formal models o f real systems usually requires translating inform al descriptions into a chosen specification formal ism, and usually takes a large amount of time, oft en months or years, without even starting a formal analysis. When publishing the results on a formal analysis in a scientific paper, details of the mo del have to be skipped due to lack of space, and o ften the lessons learnt from modelling are not dis cussed since they are not the main focus of the pa per. The workshop aims at discussing exactly these unmentioned lessons.
\n\nThe workshop emp hasises modelling over verification. In particular , we invite papers that present full Models of Rea l Systems, which may lay the basis for future form al analysis. The workshop will bring together rese archers from different communities that all aim at verifying real systems and are developing formal models for such systems. Areas where large models often occur are within networks, (trustworthy) sys tems and software verification (from byte code up to programming- and specification languages). An a im of the workshop is to present different modelli ng approaches and discuss pros and cons for each o f them.
\nSubmissions must be unpublished and not be submitted for publication elsewhere. Appendices (of arbitrary length) can be used to present all details of a formalised model ; the appendices will be part of the proceedings. In case a formal model is presented that is modell ed in some formalism or tool, these models have to be submitted as well. They will be published as p art of the proceedings, and will be made available in our Repository of Models for Formal Analysis of Real Systems. Submission de adline: Friday 13 January 2017.
\n