Aim: Logics and techniques for automated reasoning have often been<br>developed with formal analysis and formal verification in mind. To<br>show applicability, toy examples or tiny case studies are typically<br>presented in research papers. Since the theory needs to be developed<br>first, this approach is reasonable.<br>However, to show that a developed approach actually scales to real<br>systems, large case studies are essential. The development of formal<br>models of real systems usually requires a perfect understanding of<br>informal descriptions of the system–sometimes found in RFCs or other<br>standard documents–which are usually just written in English. Based on<br>the type of system, an adequate specification formalism needs to be<br>chosen, and the informal specification translated into it. Abstraction<br>from unimportant details then yields an accurate, formal model of the<br>real system.<br>The process of developing a detailed and accurate model usually takes<br>a large amount of time, often months or years; without even starting a<br>formal analysis. When publishing the results on a formal analysis in a<br>scientific paper, details of the model have to be skipped due to lack<br>of space, and often the lessons learnt from modelling are not<br>discussed since they are not the main focus of the paper.<br>The workshop aims at discussing exactly these unmentioned lessons.<br>Examples are:<br>* Which formalism is chosen, and why?<br>* Which abstractions have to be made and why?<br>* How are important characteristics of the system modelled?<br>* Were there any complications while modelling the system?<br>* Which measures were taken to guarantee the accuracy of the model?<br>The workshop emphasises modelling over verification. In particular, we<br>invite papers that present full Models of Real Systems, which may lay<br>the basis for future formal analysis. The workshop will bring together<br>researchers from different communities that all aim at verifying real<br>systems and are developing formal models for such systems. Areas where<br>large models often occur are within networks, (trustworthy) systems<br>and software verification (from byte code up to programming– and<br>specification languages). An aim of the workshop is to present<br>different modelling approaches and discuss pros and cons for each of them.<br>
Abbrevation
MARS
City
Suva
Country
Fiji
Deadline Paper
Start Date
End Date
Abstract