| Monday June 22 | Tuesday June 23 | |
|---|---|---|
| Modelling and Analysis of Communicating Systems | ||
| Abstract Behavioral Specification | ||
| Theory and Practice of Runtime Verification |
Monday 22nd June
Modelling and Analysis of Communicating Systems
Tutors:
Jan Friso Groote (Eindhoven University of Technology),
Mohammad Mousavi (Halmstad University, Sweden),
Tim Willemse (Eindhoven University of Technology)
Time and Place: 22nd June, 9:00 (full day)
Brief description :
This full day tutorial addresses the issue of formal modeling and verification of distributed and concurrent systems based on the recent book Modeling and Analysis of Communicating Systems that appeared in the summer of 2014. The theory in the book is developed with as major guideline how to model and verify real life behaviour. It rests on two pillars, namely process algebras for behavioural description and modal logic to characterise requirements. As data is indispensable when describing realistic systems, both formalisms are endowed with a whole range of data types, including functions, sets and reals. Timed behaviour can also be expressed in both the algebra and the logic.
An important purpose of the tutorial is to give an overview of the techniques addressed in the book to mathematically verify the correctness of communicating systems. There are two major approaches. The first one is by proving that an implementation behaves the same (in the sense of e.g. branching bisimulation) to the specification. For these normal forms, tau-confluence and especially the Cones and Foci method are indispensible. The second one is to verify that modal formulas are valid for given processes, for which parameterised boolean equation systems are essential.
The theory is implemented in the mCRL2 toolset, which is freely available under the extremely liberal Boost license. This toolset can be used to prove behavioural equivalences, check the validity of modal formulas, visualise behaviour in various ways, and of course also to do normal matters such as simulating behaviour and generating or reducing state spaces. The toolset has been used to design and analyse a plethora of applications, including control systems at CERN. Experience shows that the quality of programs developed using such tools goes up ten-fold.
Additional message from the Tutorial presenter:
Dear participant,
In the morning I would like to spend some time on
specifying behaviour as finite state automata, behavioural reductions
and the use of the mCRL2 toolset. In particular I would like to
analyse Peterson’s algorithm as I found it on Wikipedia (it has now
been changed).
In the afternoon I would like to spend time on the modal mu-calculus
with data to specify behavioural requirements. As an assignment I would
like to design a small software controller and show that it meets all
desired requirements. The choice is up to you, but a suggestion could
be a controller to open and close a bridge. The controller must consist
of three parallel components. One to control the user interface, one
to control the bridge, and one to control safety barriers and traffic
lights.
In order to prepare for this tutorial I would appreciate if you could
bring a copy of the book Modeling and Analysis of Communicating Systems
(https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems).
In case you do not manage to obtain a copy in time, let me know. Furthermore,
you need a computer, with the mCRL2 toolset installed (www.mcrl2.org).
Tuesday 23nd June
Abstract Behavioral Specifications
Tutors:
Reiner Hähnle (Technische Universität Darmstadt),
Einar Broch Johnsen (University of Oslo)
Time and Place: 23rd June, 14:00 (half day)
Brief description :
ABS (for abstract behavioral specification) is a formal and executable language for modelling feature-rich, concurrent, object-oriented systems at an abstract, yet precise level. ABS has a clear and simple concurrency model that integrates tightly coupled as well as actor-style distributed communication. ABS abstracts away from specific datatype, I/O or scheduler implementations, but is a fully executable language and has code generators for Java, Haskell, Erlang, and Maude.
ABS supports product line-based software development by relating feature specifications to executable models. Thus it allows gapless modelling of product lines from feature analysis down to executable code. ABS also can model properties of its runtime environment in the form of abstract deployment components. These can be related to cost annotations and reflected into cost-sensitive scheduling instructions, which makes ABS ideally suited for computationally precise modelling of applications running in the cloud.
ABS has been designed with formal analysability in mind. This makes it possible, for example, to perform automatic resource estimation, deadlock analysis, and even functional verification of concurrent ABS models. In the tutorial we present the most important language features of ABS and illustrate them by examples. We will also demonstrate parts of the ABS tool chain, including code generation, code animation, deadlock analysis, and resource analysis. Participants will be able to download the ABS tools in the form of an Eclipse plugin and try them out hands-on, if they wish.
Theory and Practice of Runtime Verification
Tutors:
Martin Leucker (Universität zu Lübeck)
Daniel Thoma (Universität zu Lübeck)
Time and Place: 23rd June, 09:00 (full day)
Brief description :
In this tutorial we give an introduction to the field of Runtime Verification. More specifically, we give a comprehensive and coherent assessment to Linear Temporal Logic-based monitor synthesis approaches. We cover both rewriting and automata-based techniques, each from a propositional as well as from a data perspective. Beyond a formal account we present applications, especially in the area of testing. To this end, we give a practical introduction to the tool JUnitRV, which combines traditional unit testing for Java with Runtime Verification techniques.
The tutorial is tailored towards researches in theoretical foundations as well as towards users of formal methods.