A Perspective on "CCS Expressions, Finite State Processes, and Three Problems of Equivalence"

With the publication of the Kannellakis-Smolka 1983 PODC paper, Kanellakis and Smolka pioneered the development of efficient algorithms for deciding behavioral equivalence of concurrent and distributed processes, especially bisimulation equivalence. Bisimulation is the cornerstone of the process-algebraic approach to modeling and verifying concurrent and distributed systems. They also presented complexity results that showed certain behavioral equivalences are computationally intractable. Collectively, their results founded the subdiscipline of algorithmic process theory, and established the associated bridges between the European research community, whose focus at the time was on process theory, and that of the US, with a rich tradition in algorithm design and computational complexity, but to whom process theory was largely unknown.

Gobra: Modular Specification and Verification of Go Programs

Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives.We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations.

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present , a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that is well-suited for both horizontal and vertical modular reasoning.

A Method to Analyze Predicate Transition Nets Using SPIN Model Checker

High-level Petri nets (HLPNs) are a formal method for studying concurrent and distributed systems and have been widely used in many application domains. However, their strong expressive power hinders their analyzability. In this paper, we present a new transformational analysis method for analyzing a special class of HLPNs — predicate transition (PrT) nets. This method extends and improves our prior results by covering more PrT net features including full first-order logic formulas and exploring additional alternative translation schemes. This new analysis method is supported by a tool chain — front-end PIPE[Formula: see text] for creating and simulating PrT nets and back-end SPIN for model checking safety and liveness properties. We have applied this method to two benchmark systems used in annual Petri net model checking contest 2015. We discuss several properties and show the detailed model checking results in one system.

Preface to special issue: behavioural types

This is the first part of a two-part special issue on Behavioural Types, which has its origin in a workshop we organized in April 2011, in Lisbon. The aim of the workshop was to bring together the active and expanding community of researchers using type-theoretic approaches to describe and analyse behavioural aspects of software. A particular concern of this field is the identification and description of structured communication in concurrent and distributed systems, but behavioural typing also addresses issues of liveness, fairness, deadlock-freedom, security, observable equivalence and typestate.

A COMPREHENSIVE SURVEY OF PETRI NET MODELING IN SOFTWARE ENGINEERING

Petri nets, a formal model for concurrent and distributed systems, have been widely applied in system modeling and analysis in almost every branch of computer science and many other scientific and engineering disciplines in the past half century. In this comprehensive survey, we review some major developments of Petri nets that have enhanced their modeling capabilities and in particular the methods to incorporate well-known software engineering development paradigms in Petri nets to support general software system modeling.