Schedule
| Wednesday, March 4 | ||
|---|---|---|
| 19:00 | Pre-Dinner at Restaurant China, Markt 20, Kerkrade | |
| Thursday, March 5 | ||
| 09:00-09:15 | Opening (Saal 6) | |
| Session 1 | Saal 6 | Saal 14 |
| 09:15-10:00 | Stefan Rieger (TWT Stuttgart): Formal Modeling and Analysis in Industry – Exemplary Application to the European Train Control System (ETCS) | Sascha Fendrich (Bamberg): Nondeterministic Modal Interfaces |
| 10:00-10:45 | Grigory Markin (Lübeck): A New Refinement Strategy for CEGAR-based Industrial Model Checking | Discussion: Perspective-Based Specifications with Different Alphabets (Chair: Ferenc Bujtor, Augsburg) |
| 10:45-11:00 | Coffee Break | |
| Session 2 | Saal 6 | Saal 14 |
| 11:00-11:45 | Hauke Baller (Braunschweig): CCSBerry – A Concurrency Theory Experimentation Kit | Christina Rickmann (Berlin): Mechanical Verification of FLP |
| 11:45-12:30 | Discussion: Teaching Concurrency (Chair: Holger Hermanns, Saarbrücken; Saal 6) |
|
| 12:30-14:00 | Lunch | |
| Session 3 | Saal 6 | Saal 14 |
| 14:00-14:45 | Normann Decker (Lübeck): On an Extension of Freeze LTL Part I – Decidability | Christoph Wagner (Berlin): An Introduction to Psi-Calculi |
| 14:45-15:30 | Daniel Thoma (Lübeck): On an Extension of Freeze LTL Part II – Complexity | Paul-David Brodmann (Berlin): Distributability of Asynchronous Process Calculi |
| 15:30-16:00 | Coffee Break | |
| Session 4 | Saal 6 | Saal 14 |
| 16:00-16:45 | Evgeny Erofeev (Oldenburg): Binary Words Synthesis with Petri Nets | Tobias Prehn (Berlin): Time to Synchronise? |
| 16:45-17:30 | David Karcher (Berlin): Higher Order Dynamics in Event Structures | Tobias Heindel (Edinburgh): Some Real Calculations for Continuous Time Preferential Attachment Networks |
| 18:00 | Guided Tour of Rolduc Abbey (meet at reception) | |
| 19:00 | Dinner at Restaurant Zwaantje, Rolduc | |
| Friday, March 6 | ||
| 09:00-10:00 | Invited Talk by Marieke Huisman (University of Twente): Verification of Concurrent Software (Saal 6) |
|
| Session 5 | Saal 6 | Saal 14 |
| 10:00-10:45 | Holger Hermanns (Saarbrücken): Probabilistic Termination | Xiaoxiao Yang (Aachen): Proving Linearizability and Progress of Concurrent Objects by Bisimulation |
| 10:45-11:00 | Coffee Break | |
| Session 6 | Saal 6 | Saal 14 |
| 11:00-11:45 | Lars Luthmann (Braunschweig): Input/Output Conformance Testing of Modal Interface Automata | Henning Kerstan (Duisburg-Essen): Behavioral Metrics via Functor Lifting |
| 11:45-12:30 | Benedikt Nordhoff (Münster): Concurrent Security on the Rocks with a Dash of DPN | Felix Freiberger (Saarbrücken): Interacting with Concurrency Theory |
| 12:30-13:00 | Business Meeting (Saal 6) | |
| 13:00-14:00 | Lunch | |
Invited Talk
- Marieke Huisman (University of Twente): Verification of Concurrent Software
This talk presents the VerCors approach to verification of concurrent software. First we discuss why verification of concurrent software is important, but also challenging, and we show how permission-based separation logic allows one to reason about multithreaded Java programs in a thread-modular way. We discuss in particular how we extend the logic to reason about functional properties in a concurrent setting. Further, we show how the approach is also suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is used to verify functional correctness properties of OpenCL kernels.
Discussions
- Perspective-Based Specifications with Different Alphabets (proposed by Ferenc Bujtor, Augsburg)
This discussion is about future work on Modal Interface Automata (MIA) as presented in the previous talk by Sascha Fendrich, titled „Nondeterministic Modal Interfaces“. MIA is our latest merge between Kim Larsen’s Modal Transition Systems (may- and must-transitions) and de Alfaro and Henzinger’s Interface Automata (inputs and outputs). MIA’s refinement allows for extension of alphabets during refinement and is equipped with the appropriate conjunction. This allows to combine specifications with different alphabets, thus supporting perspective-based specification, since separate aspects of a system often concern different actions. In the current MIA approach, a conjunct allows but ignores actions unknown to it: If two conjuncts require one of their respective actions (foreign to the other conjunct), then in a common refinement both actions must be implemented. Furthermore, after one of them has been performed, the other one has still to be offered. From a technical perspective, this alphabet extension has all desired properties, but there are applications where a different approach would be more appropriate. For example, a foreign action might suspend a conjunct until a special resume-action is performed. After a short introduction to the setting, some associated ideas and examples, the discussion should revolve around the desired properties and possible meanings of conjunction with different alphabets. The hope is that participants contribute interesting examples for and ideas about perspective-based specification.
- Teaching Concurrency (proposed by Holger Hermanns, Saarbrücken)
Presentations
- Hauke Baller (Braunschweig): CCSBerry – A Concurrency Theory Experimentation Kit
Before last term, we took a close look at our concurrency theory lecture and extended it by a few ideas to (1) raise the students’ attention to current research projects in the field of concurrency theory and (2) increase the number of students attending the course by adding some fun, yet educational, elements. To tackle goal (1), we introduced advanced lectures dealing with current research topics, delivering an insight in recent research challenges. In order to address the second goal, we added some practical hands on elements to the exercise lessons, which was initialized by the talk of Holger Hermanns at Königswinter, August 2013. Therefore, we developed CCSBerry, a CCS-like language, enriched by, e.g., display output, delays and variables. CCSBerry compiles to Python scripts, which are executed on several “Raspberry Pis” equipped with a small display and connected via a local network. Due to the obvious distributed setup, executions of concurrent processes are represented in an intuitive and believable fashion, compared to traditional approaches like simulated concurrency on single machines by software tools.In my talk, I would like to give a small overview of how we used CCSBerry for teaching concurrency theory. Furthermore, I will point out where CCSBerry differs from CCS. There is also ongoing work in extending and improving CCSBerry, e.g., by adding more concepts of (other) process calculi.
- Paul-David Brodmann (Berlin): Distributability of Asynchronous Process Calculi
We analyze three process calculi with regard to their ability to distribute a process term onto different locations while maintaining the same behavior. This is especially relevant for distributed systems. The limiting factor for distributability are so called Synchronization patterns. We show that neither the Actor pi-Calculus, the Join-Calculus nor the Localized pi-Calculus contain these Synchronization patterns. Therefore the calculi share a similar degree of distributability. With this knowledge we present distributability preserving encodings, mappings between process calculi, which show that the calculi have the same relative expressive power. The encodings fulfill the common quality criteria.
- Normann Decker (Lübeck): On an Extension of Freeze LTL Part I – Decidability
We present an extension of Freeze LTL, a temporal logic equipped with registers, over multi-attributed data words. Each position in a multi-attributed data word carries a letter from a finite alphabet and additionally assigns a data value to a fixed, finite set of attributes. The satisfiability problem of Freeze LTL is undecidable if more then one register is available or tuples of data values can be stored and compared arbitrarily. Our extension allows for specifying a dependency relation on attributes. These dependencies restrict in a flexible way how collections of attribute values can be stored and compared. This new dimension of flexibility is orthogonal to, e.g., the number of registers or the available temporal operators. In this setting we characterise precisely the type of dependency relations that maintain decidability of the logic. Decidability results are obtained by a translation to nested counter systems.
- Evgeny Erofeev (Oldenburg): Binary Words Synthesis with Petri Nets
Petri net region theory investigates the conditions under which a labelled transition system is the reachability graph of a Petri net. Solvability of lts with Petri net requires event separation and can be explained by linear algebra. We are looking for a direct and more efficiently implementable characterisation. Starting with a simple case of an lts in the form of finite line (a word), and only two labels (transitions of Petri net) we study necessary and sufficient conditions for (un)solvability of this lts with Petri net. In this talk the following question is addressed: given a certain word over two-letters alphabet is there a generating Petri net with the reachability graph isomorphic to this word?
- Sascha Fendrich (Bamberg): Nondeterministic Modal Interfaces
Interface theories are employed in the component-based design of concurrent systems. They often emerge as combinations of Interface Automata (IA) and Modal Transition Systems (MTS), e.g., Nyman et al.’s IOMTS, Bauer et al.’s MIO, Raclet et al.’s MI or our MIA. We generalise MI to nondeterministic interfaces, for which we resolve the longstanding conflict between unspecified inputs being allowed in IA but forbidden in MTS. With this solution we achieve, in contrast to related work, an associative parallel composition, a compositional preorder, a conjunction on interfaces with dissimilar alphabets supporting perspective-based specifications, and a quotienting operator for decomposing nondeterministic specifications in a single theory.
- Felix Freiberger (Saarbrücken): Interacting with Concurrency Theory
This presentation reports on a novel web application allowing to interactively experience aspects of concurrency theory and concurrency practice. It especially targets a student audience working with CCS to model concurrent processes and/or working with pseuCo to write first concurrent programs. Apart from editing pseuCo and CCS files, the app visualizes their underlying labelled transition system semantics. In addition it supports minimization and both automatic and semi-automatic graph layout, all of which works even for partially explored fragments of a potentially infinite-state semantics. The app runs out-of-the-box in any customary web browser, easing deployment especially for teaching purposes.
- Tobias Heindel (Edinburgh): Some Real Calculations for Continuous Time Preferential Attachment Networks
Preferential attachment is a simple network model that intuitively explains how the rich get richer, papers get cited, or contacts evolve on social networks; formally, preferential attachment generates power law distributions such that the probability of a node to have degree k is proportional to k^c. How can we calculate the expected number of nodes of a certain degree in function of time, exactly? The proposed answer: automatically generate the right differential equations and calculate their solution; so we just need the right ODEs, dubbed moment semantics, which we can actually generate for all moments of random variables that count so-called motifs, e.g., nodes of a certain degree.
- Holger Hermanns (Saarbrücken): Probabilistic Termination
We propose a framework to prove almost sure termination for probabilistic programs with real valued variables. It is based on ranking supermartingales, a notion analogous to ranking functions on nonprobabilistic programs. The framework is proven sound and complete for a meaningful class of programs involving randomization and bounded nondeterminism. We complement this foundational insight by a practical proof methodology, based on sound conditions that enable compositional reasoning and are amenable to a direct implementation using modern theorem provers. This is integrated in a small dependent type system, to overcome the problem that lexicographic ranking functions fail when combined with randomization. Among others, this compositional methodology enables the verification of probabilistic programs outside the complete class that admits ranking supermartingales.
- David Karcher (Berlin): Higher Order Dynamics in Event Structures
Event Structures (ESs) are a concurrency model introduced by Winskel, consisting of atomic and nonrecurring events and relations between them, like causality or binary conflict. So far the causal dependencies were static, we present a dynamised version, called Dynamic Causality ESs (DCES), in which events may change (i.e. add or drop) causal predecessors of other events. Comparing DCESs regarding expressiveness to many well known ESs we discovered the incomparability of DCESs to van Glabbeeks ESs for Resolvable Conflicts. Finally we present a canonical generalisation of DCESs and show that it is strictly more expressive than ESs for Resolvable Conflicts, which can give semantics to general petri nets.
- Henning Kerstan (Duisburg-Essen): Behavioral Metrics via Functor Lifting
Behavioral (pseudo)metrics are a relaxation of behavioral equivalences: instead of requiring two states of a system (e.g. DFA) to be behaviorally equivalent (e.g. bisimilar), we are satisfied if they are close to each other, which we express via a pseudometric on states. While this can be done separately for each type of system, we propose a general framework to obtain these pseudometrics for systems which are coalgebras for Set-functors. The crucial step is, if we are given a pseudometric on a set X, to define a suitable pseudometric on FX (where FX could be e.g. countable subsets of X or probability distributions on X). Our approach for this is a generalization of the Kantorovich/Wasserstein-distances for probability distributions. We obtain a functor on the category of pseudometric spaces, which we call a lifting of the original functor. Given such a lifting, we derive a fixed-point characterization of a behavioral pseudometric which satisfies the (desirable) property that two equivalent states have distance 0.
- Lars Luthmann (Braunschweig): Input/Output Conformance Testing of Modal Interface Automata
Testing principles for input/output conformance (ioco) already exist for Labeled Transition Systems (LTS), however LTS do not support distinguishing between mandatory and optional behavior. Our proposed testing theory relies on Modal Interface Automata (MIA) as a behavioral specification formalism supporting mandatory and optional behavior by using may- and must-modality. In particular, MIA constitute a restricted, yet fully expressive subclass of input/output-labeled modal transition systems, guaranteeing desirable refinement and compositionality properties. With MIA, we are also able to build a modal version of the ioco relation being preserved under MIA refinement. Modal-ioco is proven correct in the sense that it coincides with traditional ioco to hold for every derivable implementation variant. Based on these results, a modal conformance testing framework can be established. During the talk, we introduce modal-ioco for MIA and show its connection to ioco theory. Additionally, we sketch a promising conjecture on how modal-ioco may be preserved under parallel composition.
- Grigory Markin (Lübeck): A New Refinement Strategy for CEGAR-based Industrial Model Checking
This talk presents a novel refinement strategy in the context of counterexample-guided abstraction refinement (CEGAR) based model checking. More specifically, the shown approach builds on lazy abstraction in the context of predicate abstraction. While typically, the concept of interpolants is used for refinement, the current paper employs unsatisfiability cores together with weakest preconditions. Hence, the new refinement technique is especially applicable in the setting where interpolants are hard to compute, such as for McCarthy’s theory of arrays and especially for the theory of fixed-width bit-vectors. The approach is implemented within a model checking tool developed for the verification of industrial critical systems. It is shown that the new refinement strategy outperforms current refinement strategies for the combination of the theories mentioned above.
- Benedikt Nordhoff (Münster): Concurrent Security on the Rocks with a Dash of DPN
This talk is concerned about information flow security. I’ll give a brief overview of the basic problem especially in the presence of concurrency, where covert channels like timing can lead to explicit information leaks. I will present the Low Security Observational Determinism (LSOD) security property and a PDG based analysis approach, with integrated DPN analyses, that certifies LSOD.
- Tobias Prehn (Berlin): Time to Synchronise?
Process calculi can be used to model distributed systems. Some of these calculi allow for unwanted hidden synchronisation. The consideration of time can add the possibility for a distributed system to act synchronously. We formally analyse how time can be utilised to synchronise and how much synchronisation power can be achieved this way in the context of the distributed pi calculus. Furthermore, we discuss the system assumptions under which synchronisation on time is possible.
- Stefan Rieger (TWT Stuttgart): Formal Modeling and Analysis in Industry – Exemplary Application to the European Train Control System (ETCS)
The goal of ETCS is the unification of the European rail network allowing train operators to use a rail vehicle equipped with a single signalling system to operate throughout Europe. The European research project openETCS aims to provide a formalisation and a prototypical implementation of the ETCS specification. In this talk we will show how colored Petri nets (CPNs) can be used to model the communication between the ETCS on-board unit with the driver and the track-side control centre. The model enables an early validation of the specification and the analysis of fundamental properties (such as deadlocks) by applying model checking. We will show how a CPN can be derived from the specification and which difficulties may arise in this process. The modelling tool applied is CPN Tools. Based on a transformation of the CPNs to low level Petri nets the model checker LoLA (Low Level Petri Net Analyzer) can be applied for verification.
- Christina Rickmann (Berlin): Mechanical Verification of FLP
The impossibility of distributed consensus-originally proven by Fisher, Lynch and Paterson-is a fundamental result in computer science and has to our knowledge not yet been fully mechanically verified. We present a formalization of Völzer’s paper A constructive proof for FLP using the interactive theorem prover Isabelle/HOL. We focus on the main differences between our proof and Völzer and summarize necessary design decisions in our formal approach. Additionally we proof fairness of the constructed non-terminating execution for the first time.
- Daniel Thoma (Lübeck): On an Extension of Freeze LTL Part II – Complexity
We investigate the complexity of our extension of Freeze LTL introduced in Part I. As satisfiability of Freeze LTL is known to be already non-primitive recursive we require complexity classes beyond. We first outline the necessary background on ordinal numbers and fast-growing functions. We then prove lower and upper bounds for coverability in nested counter systems and transfer these bounds over to our extension of Freeze LTL. Combining these results we obtain F_{ε_0}-completeness of our extension.
- Christoph Wagner (Berlin): An Introduction to Psi-Calculi
In this talk I will give a quick introduction to the Psi-Calculi. The Psi-Calculi evolved out of the need for applied models rather than minimalistic ones. Beginning from 2008 it evolved into a rich meta-framework for process calculi, being able to be instantiated to act like, e.g. the Pi, Spi, or Fusion-Calculus.
- Xiaoxiao Yang (Aachen): Proving Linearizability and Progress of Concurrent Objects by Bisimulation
We present concurrent object bisimulation, a tailored instance of branching (akin: stutter) bisimulation, for verifying linearizability – a key correctness criterion for concurrent objects. Our approach is based on verifying an object program against a concurrent abstract program in which object methods are abstracted according to linearization points. We show that in this setting, our bisimulation is divergence-sensitive. This allows for exploiting our bisimulation relation for various progress properties such as lock-, wait-, and obstruction-freedom. Our results imply that both linearizability and progress properties can be preserved in our setting. For automated verification, branching bisimulation checking techniques thus suffice for checking linearizability and progress. Based on this method, we have successfully verified various classic algorithms, some of
which are used in the java.util.concurrent package.