In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specifications. For synchronous distributed systems, the synthesis problem is well known to be undecidable. For asynchronous systems, the boundary between decidable and undecidable synthesis problems is a long-standing open question. We study the problem in the setting of Petri games, a framework for distributed systems where asynchronous processes are equipped with causal memory. Petri games extend Petri nets with a distinction between system places and environment places. The components of a distributed system are the players of the game, represented as tokens that exchange information during each synchronization. Previous decidability results for this model are limited to local winning conditions, i.e., conditions that only refer to individual components. In this paper, we consider global winning conditions such as mutual exclusion, i.e., conditions that refer to the state of all components. We provide decidability and undecidability results for global winning conditions. First, we prove for winning conditions given as bad markings that it is decidable whether a winning strategy for the system players exists in Petri games with a bounded number of system players and one environment player. Second, we prove for winning conditions that refer to both good and bad markings that it is undecidable whether a winning strategy for the system players exists in Petri games with at least two system players and one environment player. Our results thus show that, on the one hand, it is indeed possible to use global safety specifications like mutual exclusion in the synthesis of distributed systems. However, on the other hand, adding global liveness specifications results in an undecidable synthesis problem for almost all Petri games.

The correctness of networks is often described in terms of the individual data flow of components instead of their global behavior. In software-defined networks, it is far more convenient to specify the correct behavior of packets than the global behavior of the entire network. Petri nets with transits extend Petri nets and Flow-LTL extends LTL such that the data flows of tokens can be tracked. We present the tool AdamMC as the first model checker for Petri nets with transits against Flow-LTL. We describe how AdamMC can automatically encode concurrent updates of software-defined networks as Petri nets with transits and how common network specifications can be expressed in Flow-LTL. Underlying AdamMC is a reduction to a circuit model checking problem. We introduce a new reduction method that results in tremendous performance improvements compared to a previous prototype. Thereby, AdamMC can handle software-defined networks with up to 82 switches.

Abstract The manual implementation of local controllers for autonomous agents in a distributed and concurrent setting is an ambitious and error-prune task. Synthesis algorithms, however, allow for the automatic generation of such controllers given a formal specification of the system’s goal. Recently, high-level Petri games were introduced to allow for a concise modeling technique of distributed systems with a safety objective. One way of solving these games is by a translation to low-level Petri games and applying an existing solving algorithm. In this paper we present a new solving technique for a subclass of high-level Petri games with a single uncontrollable player, a bounded number of controllable players, and a local safety objective. The technique exploits symmetries in the high-level Petri game. We report on encouraging experimental results of a prototype implementation generating the reduced state space. The results for four existing and one new benchmark family show a state space reduction by up to three orders of magnitude.

Abstract We present a history of Hoare’s logic.

Abstract The dynamic behavior of a car can be modeled as a hybrid system involving continuous state changes and discrete state transitions. We show that the control of safe (collision free) lane change maneuvers in multi-lane traffic on highways can be described by finite state machines extended with continuous variables coming from the environment. We use standard theory for controller synthesis to derive the dynamic behavior of a lane-change controller. Thereby, we contrast the setting of interleaving semantics and synchronous concurrent semantics. We also consider the possibility of exchanging knowledge between neighboring cars in order to come up with the right decisions. Finally, we address compositional verification using an assumption-guarantee paradigm.

Abstract We investigate design-level structural transformations that aim at easier subsequent verification of real-time systems with shared data variables, modelled as networks of extended timed automata (ETA). Our contributions to this end are the following: (1) we first equip ETA with an operator for layered composition , intermediate between parallel and sequential composition. Under certain non-interference and/or precedence conditions imposed on the structure of the ETA networks, the communication closed layer (CCL) laws and associated partial-order (po-) and (layered) reachability equivalences are shown to hold. (2) Next, we investigate (under certain cycle conditions on the ETA) the (reachability preserving) transformations of separation and flattening aimed at reducing the number of cycles of the ETA. (3) We then show that our separation and flattening in (2) may be applied together with the CCL laws in (1), in order to restructure ETA networks such that the verification of layered reachability properties is rendered easier. This interplay of the three structural transformations (separation, flattening, and layering) is demonstrated on an enhanced version of Fischer’s real-time mutual exclusion protocol for access to multiple critical sections.

Abstract This paper adopts the communication closed layer (CCL) concept of Elrad and Francez to the formal reasoning of randomized distributed algorithms. We do so by enriching probabilistic automata (PA) with a layered composition operator, an intermediate between parallel and sequential composition. Layered composition is used to establish probabilistic counterparts of the CCL laws that exploit independence and/or precedence conditions between the constituent PA. The probabilistic CCL laws enable partial order (po-) equivalence when layered composition is replaced by sequential composition. Such po-equivalence induces a purely syntactic partial-order state space reduction via layered separation in compositions of PA while preserving probabilistic next-free linear-time properties. The feasibility of such layered separation is demonstrated on a randomized mutual exclusion algorithm by Kushilevitz and Rabin, complementing an algebraic approach (for analyzing this algorithm) by McIver, Gonzalia, Cohen, and Morgan.

Abstract We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed reactive systems . To this end, we propose a specific UML profile for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by CSP jassda , an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts.

Security automata are a variant of Büchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification language combining Communicating Sequential Processes (CSP) and Object-Z (OZ), to specify security automata, formalize their combination with target systems, and analyze the security of the resulting system specifications. We provide theoretical results relating CSP-OZ specifications and security automata and show how refinement can be used to reason about specifications of security automata and their combination with target systems. Through a case study, we provide evidence for the practical usefulness of this approach. This includes the ability to specify concisely complex operations and complex control, support for structured specifications, refinement, and transformational design, as well as automated, tool-supported analysis.

The design of intricate real-time systems typically involves several notations that describe the system at different levels of abstraction. Graphical notations inspired by timing diagrams are helpful at the requirements level, structured automata are common at the design level and dedicated languages are used at the programming level. The question arises how these different notations are linked together in a semantically meaningful way. The author argues that a logic-based approach is making a real contribution.

Readiness and failure semantics are studied in the setting of Algebra of Communicating Processes (ACP). A model of process graphs modulo readiness equivalence, respectively, failure equivalence, is constructed, and an equational axiom system is presented which is complete for this graph model. An explicit representation of the graph model is given, the failure model, whose elements are failure sets. Furthermore, a characterisation of failure equivalence is obtained as the maximal congruence which is consistent with trace semantics. By suitably restricting the communication format in ACP, this result is shown to carry over to subsets of Hoare’s Communicating Sequential Processes (CSP) and Milner’s Calculus of Communicating Systems (CCS). Also, the characterisation implies a full abstraction result for the failure model. In the above we restrict ourselves to finite processes without $\tau $-steps. At the end of the paper a comment is made on the situation for infinite processes with $\tau $-steps: notably we obtain that failure semantics is incompatible with Koomen’s fair abstraction rule, a proof principle based on the notion of bisimulation. This is remarkable because a weaker version of Koomen’s fair abstraction rule is consistent with (finite) failure semantics.

Program transformations are proposed as a means of providing fair parallelism semantics for parallel programs with shared variables. The transformations are developed in two steps. First, abstract schedulers that implement the various fairness policies are introduced. These schedulers use random assignments z := ? to represent the unbounded nondeterminism induced by fairness. Concrete schedulers are derived by suitably refining the ?. The transformations are then obtained by embedding the abstract schedulers into the parallel programs. This embedding is proved correct on the basis of a simple transition semantics. Since the parallel structure of the original program is preserved, the transformations also provide a basis for syntax-directed proofs of total correctness under the fairness assumption. These proofs make use of infinite ordinals.

Transition systems as proposed by Hennessy & Plotkin are defined for a series of three languages featuring concurrency.The first has shuffle and local nondeterminancy, the second synchronization merge and local nondeterminacy, and the third synchronization merge and global nondeterminacy.The languages are all uniform in the sense that the elementary actions are uninterpreted.Throughout, infinite behaviour is taken into account and modelled with infinitary languages in the sense of Nivat.A comparison with denotational semantics is provided.For the first two languages, a linear time model suffices; for the third language a braching time model with processes in the sense of De Bakker & Zucker is described.In the comparison an important role is played by an intermediate semantics in the style of Hoare & Olderog's specification oriented semantics.A variant on the notion of ready set is employed here.Precise statements are given relating the various semantics in terms of a number of abstraction operators.

This paper presents a new characterization of applicability and limitations of Hoare's logic. We consider a programming language LPas consisting of nondeterministic programs with a Pascal-like procedure concept and prove as our main theorem: Admissible sublanguages L of LPas have a sound and relatively complete Hoare logic if and only if all programs in L have regular formal call trees. Moreover, we present an explicit Hoare calculus for L whenever such a Hoare logic exists. Our theorem generalizes Clarke's results on completeness and incompleteness for languages with procedures [Cl 79] and improves Lipton's characterization of Hoare's logic which cannot deal with nondeterminism and does not provide explicit calculi [Li 77].