Florian Lercher visiting Swansea

Florian Lercher (Ausburg University is visiting Swansea). Today he is giving a talk on “Compositional Verification of Communicating UML State Machines”.

When dealing with large concurrent systems, verification methods such as model checking usually do not scale up well. This is because they need to explore the global state space of the system, which can grow exponentially with the number of concurrent components.Compositional verification methods, on the other hand, scale linearly with the number of components.To achieve this, compositional methods first prove local properties for each individual component and then compose these into a global property of the system.

We develop a compositional verification method for asynchronously communicating state machines.To this end, we modify the approach by de Roever et al. that works with synchronous communication.Our verification method follows the assumption-commitment paradigm, meaning that a property consists of an assumption about the environment and a commitment that the program has to satisfy only if the assumption holds. Due to the design of our model, representing a system of communicating UML state machines is relatively straightforward.We implement a tool to translate a system of communicating UML state machines into our formalism and generate the necessary proof obligations in an interactive theorem prover. To demonstrate the capabilities of our approach, we apply it to several examples.

In the talk, we will verify the LCR algorithm for distributed leader election and then explore the theory behind the approach.