Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems
Extracted source text ยท arXiv 1703.05812
<!DOCTYPE HTML PUBLIC>
<html><head><title>EPTCS 244: Models for Formal Analysis of Real Systems</title>
<style>
body { width: 90%;
background: #ffee88;
margin: 0 auto;
text-align: justify;
margin-bottom: 2em; }
hr.sep { border-top: solid 1px #cc0000; }
p.indent { text-indent: 1.5em; margin-bottom: 0pt; margin-top: 0pt; }
a { text-decoration: none; }
td.fill { border-bottom: dotted 1px #cc0000; }
</style>
<script type="text/javascript">
function changeText(){
document.getElementById('sitemap').innerHTML = '<table width=100%>'+
'<tbody><tr><td align="left">'+
'<font size=-1>'+
'<b>DOI:</b> <a href="http://dx.doi.org/10.4204/EPTCS.244">'+
'10.4204/EPTCS.244</a><br>'+
'<b>ISSN:</b> 2075-2180</font><br><br><br><br><br><br><br><br><br><br><br><br>'+
'</td><td align="left" bgcolor="#ffffff"><ul>'+
'<li><a href="http://published.eptcs.org/" target="_top">Published Volumes</a>'+
'<li><a href="http://forthcoming.eptcs.org/" target="_top">Forthcoming Volumes</a>'+
'<li><a href="http://eptcs.org/" target="_top">About EPTCS</a>'+
'<li><a href="http://editors.eptcs.org/" target="_top">Editorial Board</a>'+
'<li><a href="http://hardcopy.eptcs.org/" target="_top">Ordering Hardcopy</a>'+
'<li><a href="http://info.eptcs.org/" target="_top">Information for '+
'Authors and Event Organisers</a>'+
' <ul>'+
' <li> <a href="http://style.eptcs.org/" target="_top">LaTeX style file and'+
' formatting instructions</a>'+
' <ul>'+
' <li><a href="http://eptcs.web.cse.unsw.edu.au/eptcsstyle.zip" target="_top">eptcsstyle.zip</a>'+
' </ul>'+
' <li> <a href="http://copyright.eptcs.org/" target="_top">Copyright</a>'+
' </ul>'+
'<li><a href="http://apply.eptcs.org/" target="_top">'+
'Application to Publish in EPTCS</a>'+
'<li><a href="http://login.eptcs.org/" target="_top">Login Page for Editors and Authors'+
'</ul></td></tr></tbody></table>';
}
</script>
</head>
<body>
<div id='sitemap'>
<table width=100%><tr>
<td align='left'>
<font size=-1>
<b>DOI:</b> <a href="http://dx.doi.org/10.4204/EPTCS.244">
10.4204/EPTCS.244</a><br>
<b>ISSN:</b> 2075-2180</font>
</td><td align='left'>
<input style="cursor: pointer" type='button' onclick='changeText()' value='EPTCS Site Map'/>
</td><td align='right'>
<input style="cursor: pointer" type='button' value='EPTCS Home Page'
onClick='parent.location="http://eptcs.org/"'/>
</td><td align='right'>
<input style="cursor: pointer" type='button' value='Published Volumes'
onClick='parent.location="http://published.eptcs.org/"'/>
</td><td align='right'>
<input style="cursor: pointer" type='button' value='Forthcoming Volumes'
onClick='parent.location="http://forthcoming.eptcs.org/"'/>
</td></tr></table></div>
<center>
<h1>EPTCS 244</h1>
<h1><font size=5>Proceedings 2nd Workshop on</font>
<br>Models for Formal Analysis of Real Systems
<br><font size=3>Uppsala, Sweden, 29th April 2017</font></h1>
Edited by: Holger Hermanns and Peter Höfner
</center>
<hr class=sep>
<table width=100%>
<tr><td class=fill><i><a href="#EPTCS244.0">
Preface</a></i></br>
Holger Hermanns and Peter Höfner</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.1">
Evaluating the Stream Control Transmission Protocol Using Uppaal</a></i></br>
Shruti Saini and Ansgar Fehnker</td><td align="right">1</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.2">
Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack</a></i></br>
Rob van Glabbeek and Peter Höfner</td><td align="right">14</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.3">
Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol</a></i></br>
Kaylash Chaudhary, Ansgar Fehnker and Vinay Mehta</td><td align="right">53</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.4">
Formalizing Memory Accesses and Interrupts</a></i></br>
Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe</td><td align="right">66</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.5">
Modelling and Verification of a Cluster-tree Formation Protocol Implementation for the IEEE 802.15.4 TSCH MAC Operation Mode</a></i></br>
Mahmoud Talebi, Jan Friso Groote and Conrad Dandelski</td><td align="right">117</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.6">
A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm</a></i></br>
Hubert Garavel and Lina Marsso</td><td align="right">129</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.7">
Modelling of Autosar Libraries for Large Scale Testing</a></i></br>
Wojciech Mostowski, Thomas Arts and John Hughes</td><td align="right">184</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.8">
A Benchmark on Reliability of Complex Discrete Systems: Emergency Power Supply of a Nuclear Power Plant</a></i></br>
Marc Bouissou</td><td align="right">200</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.9">
A Model-Derivation Framework for Software Analysis</a></i></br>
Bugra M. Yildiz, Arend Rensink, Christoph Bockisch and Mehmet Aksit</td><td align="right">217</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.10">
The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark</a></i></br>
Hubert Garavel and Wendelin Serwe</td><td align="right">230</td></tr>
<tr><td class=fill><i><a href="http://dx.doi.org/10.4204/EPTCS.244.11">
Towards Probabilistic Formal Modeling of Robotic Cell Injection Systems</a></i></br>
Muhammad Usama Sardar and Osman Hasan</td><td align="right">271</td></tr>
</table>
<hr class=sep><h1 align=left><a name='EPTCS244.0'>Preface</a></h1>
This volume contains the proceedings of MARS 2017, the second workshop
on <i>Models for Formal Analysis of Real Systems</i>,
held on April 29, 2017 in Uppala, Sweden, as an affiliated workshop of ETAPS 2017,
the <i>European Joint Conferences on Theory and Practice of Software</i>.
Logics and techniques for automated reasoning have often been
developed with formal analysis and formal verification in mind.
To show applicability, toy examples or tiny case studies are
typically presented in research papers. Since the theory needs
to be developed first, this approach is reasonable.
However, to show that a developed approach actually scales to
real systems, large case studies are essential.
The development
of formal models of real systems usually requires a perfect
understanding of informal descriptions of the system—sometimes
found in RFCs or other standard documents—which are usually just
written in English. Based on the type of system, an adequate
specification formalism needs to be chosen, and the informal
specification needs to be translated into it. Examples for such formalisms
include process and program algebra, Petri nets, variations of
automata, as well as timed, stochastic and probabilistic
extensions of these formalisms. Abstraction from unimportant
details then yields an accurate, formal model of the real system.
The process of developing a detailed and accurate model usually
takes a considerable amount of time, often months or years; without even
starting a formal analysis. When publishing the results on a formal
analysis in a scientific paper, details of the model usually have to be skipped
due to lack of space, and often the lessons learnt from modelling are
not discussed since they are not the main focus of the paper.
The workshop aims at discussing exactly these unmentioned lessons.
Examples are:
<ul>
<li>Which formalism is chosen, and why?</li>
<li>Which abstractions have to be made and why?</li>
<li>How are important characteristics of the system modelled?</li>
<li>Were there any complications while modelling the system?</li>
<li>Which measures were taken to guarantee the accuracy of the model?</li>
</ul>
The workshop emphasises modelling over verification. In particular, we
invited papers that present full models of real systems, which may lay
the basis for future comparison and analysis. The workshop thus intends to
bring together researchers 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) systems and software verification, from byte code up to
programming- and specification languages. An aim of the workshop is
to present different modelling approaches and discuss pros and cons
for each of them.
The body of this volume contains 11 contributions, which
were selected by the Program Committee out of 16 submissions.
Each submission was carefully reviewed by at least three members of the programme committee,
assisted by outside referees, whose help is gratefully acknowledged.
The papers presented in this volume include
formal models for
<ul>
<li><strong>(contemporary) hardware</strong>, in particular a formal model for the interpretation of memory accesses and interrupts;</li>
<li><strong>protocols</strong> such as
the Better Approach to Mobile Ad hoc Networks (B.A.T.M.A.N.) routing protocol,
a fragmentation protocol running on top of the standardised CAN bus,
the Stream Control Transmission Protocol (SCTP), and
a cluster-tree formation protocol for the IEEE 802.15.4 TSCH MAC operation mode;</li>
<li><strong>application software</strong>, including a cryptographic algorithm for message authentication,
and AUTOSAR (AUTomotive Open System ARchitecture) components;</li>
<li><strong>physical systems</strong> such as robotic cell injection, emergency power supply of a nuclear power plant,
and (generic) production cells.</li>
</ul>
To round off the contributions, this volume also presents a model-derivation framework for software analysis, which itself can be used to generate formal models.
Full specifications of the contributed models are available at
<a href="http://mars-workshop.org">http://mars-workshop.org</a>—often including executable models—so that their quality can be evaluated.
Alternative formal descriptions are encouraged, which should foster the development of
improved specification formalisms.
<br/>
<br/>
<i>Holger Hermanns</i><br/>
<i>Peter Höfner</i>
<br/>
<br/>
<br/>
<h3>Programme Committee:</h3>
<table>
<tr>
<td><a href="http://www.inrialpes.fr/vasy/people/Hubert.Garavel/">Hubert Garavel</a></td>
<td>(INRIA, France)</td>
</tr>
<tr>
<td><a href="http://www.win.tue.nl/~jfg/">Jan Friso Groote</a></td>
<td>(Eindhoven University of Technology, The Netherlands)</td>
</tr>
<tr>
<td><a href="http://depend.cs.uni-sb.de/index.php?id=166">Holger Hermanns</a></td>
<td>(Saarland University, Germany)</td>
</tr>
<tr>
<td><a href="http://www.hoefner-online.de">Peter Höfner</a></td>
<td>(Data61, CSIRO, Australia)</td>
</tr>
<tr>
<td><a href="http://spinroot.com/gerard/">Gerard Holzmann</a></td>
<td>(NASA/JPL, USA)</td>
</tr>
<tr>
<td><a href="http://www.riskspectrum.com">Pavel Krcal</a></td>
<td>(Lloyd's Register, Sweden)</td>
</tr>
<tr>
<td><a href="http://people.cs.aau.dk/~kgl/">Kim G. Larsen</a></td>
<td>(Aalborg University, Denmark)</td>
</tr>
<tr>
<td><a href="http://www.cs.bham.ac.uk/~parkerdx/">David Parker</a></td>
<td>(University of Birmingham, United Kingdom)</td>
</tr>
<tr>
<td><a href="http://www.cs.ru.nl/~fvaan/">Frits Vaandrager</a></td>
<td>(Radboud University, The Netherlands)</td>
</tr>
<tr>
<td><a href="http://www.marcelverhoef.nl">Marcel Verhoef</a></td>
<td>(European Space Agency, ESTEC, The Netherlands)</td>
</tr>
<tr>
<td><a href="http://forsyte.at/people/widder/">Josef Widder</a></td>
<td>(TU Wien, Austria)</td>
</tr>
<table>
<hr class=sep>
</body></html>