Abstract: SVA is a new tool developed by me and David Hopkins that translates a shared variable program into Hoare's CSP and analyses it on FDR. ÊI will discuss how this translation is done, the great effectiveness of FDR's compression functions on the result and a model of refinement between shared variable program fragments. As examples I will solve an open problem regarding Simpson's 4-slot algorithm and show how a finite model checking run can prove the bakery algorithm for an unbounded ticket type and an arbitrary number of nodes.

This talk is based on Chapters 18 and 19 of my new book "Understanding Concurrent Systems".

15h00-16h00: M. Goldsmith (University of Warwick), "Refinement-Friendly Semantics for Bigraphs [and their security applications]"

Abstract: Over the past decade the successful approach to specification and mechanical analysis of correctness and security properties using CSP and its refinement checker FDR has been extended to contexts including mobile ad-hoc networks and pervasive systems. But the more scope for network reconfiguration the system exhibits, the more intricate and less obviously accurate the models must become in order to accommodate such dynamic behaviour in a language with a basically static process and communication graph. Milner's Bigraph framework, on the other hand is ideally suited for describing intuitively such dynamic reconfigurations of a system and supports notions of locality and adjacency which fit it well for reasoning, for instance, about the interface between physical and electronic security; but they currently lack powerful analytic tool support. Our long-term goal is to combine the best of both approaches.

Unfortunately the canonical labelled transition system induced by the category-theoretic semantics of a bigraphical reactive system present a number of challenges to the refinement-based approach. Prominent amongst these is the feature that the label on a transition is the 'borrowed context' required to make the redex of some reaction rule appear in the augmented source bigraph; this means that any reaction which can already take place entirely within a given bigraph gives rise to a transition labelled only with the trivial identity context, equivalent to a tau transition in CCS or CSP, with the result that neither the reaction rule nor the agents involved can be distinguished. This makes it quite impossible for an observer of the transition system to determine whether such a reaction was desirable with respect to any specification.

Here we present two alternative solutions to this problem with the effect that every transition becomes labelled with the specific rule that gave rise to it and an encoding of the set of agents involved. We also motivate the work, if time allows, with some potential applications of the notation to security modelling.