International audience

Abstract We showed in a recent paper that, when verifying a modal $$\mu $$ -calculus formula, the actions of the system under verification can be partitioned into sets of so-called weak and strong actions, depending on the combination of weak and strong modalities occurring in the formula. In a compositional verification setting, where the system consists of processes executing in parallel, this partition allows us to decide whether each individual process can be minimized for either divergence-preserving branching (if the process contains only weak actions) or strong (otherwise) bisimilarity, while preserving the truth value of the formula. In this paper, we refine this idea by devising a family of bisimilarity relations, named sharp bisimilarities, parameterized by the set of strong actions. We show that these relations have all the nice properties necessary to be used for compositional verification, in particular congruence and adequacy with the logic. We also illustrate their practical utility on several examples and case-studies, and report about our success in the RERS 2019 model checking challenge.

Abstract A GALS ( Globally Asynchronous, Locally Synchronous ) system consists of several synchronous components that evolve concurrently and interact with each other asynchronously. The design of GALS systems is tedious and error-prone due to the high degree of synchronous and asynchronous concurrency present in complex architectures. In this paper, we present GRL ( GALS Representation Language ), a formal language designed to model GALS systems, for the purpose of formal verification of the asynchronous aspects. GRL combines the synchronous reactive model underlying dataflow languages and the asynchronous concurrent model underlying process algebras. We propose a translation from GRL to LNT, a value-passing concurrent language with classical process algebra flavour. This makes possible the analysis of GRL specifications using all the state-of-the-art simulation and verification functionalities provided by the CADP toolbox.

Abstract EB3 is a specification language for information systems. The core of the EB3 language consists of process algebraic specifications describing the behaviour of the entities in a system, and attribute function definitions describing the entity attributes. The verification of EB3 specifications against temporal properties is of great interest to users of EB3 . In this paper, we propose a translation from EB3 to LOTOS NT (LNT for short), a value-passing concurrent language with classical process algebra features. Our translation ensures the one-to-one correspondence between states and transitions of the labelled transition systems corresponding to the EB3 and LNT specifications. We automated this translation with the EB32LNT tool, thus equipping the EB3 method with the functional verification features available in the CADP toolbox.

Formal process languages inheriting the concurrency and communication features of process algebras are convenient formalisms to model distributed applications, especially when they are equipped with formal verification tools (e.g., model-checkers) to help hunting for bugs early in the development process. However, even starting from a fully verified formal model, bugs are likely to be introduced while translating (generally by hand) the concurrent model -- which relies on high-level and expressive communication primitives -- into the distributed implementation -- which often relies on low-level communication primitives. In this paper, we present DLC, a compiler that enables distributed code to be generated from models written in a formal process language called LNT, which is equipped with a rich verification toolbox named CADP. The generated code can be either executed in an autonomous way (i.e., without requiring additional code to be defined by the user), or connected to external software through user-modifiable C functions. We present an experiment where DLC generates a distributed implementation from the LNT model of the Raft consensus algorithm.

Abstract Motivation: Logical (Boolean or multi-valued) modelling is widely used to study regulatory or signalling networks. Even though these discrete models constitute a coarse, yet useful, abstraction of reality, the analysis of large networks faces a classical combinatorial problem. Here, we propose to take advantage of the intrinsic modularity of inter-cellular networks to set up a compositional procedure that enables a significant reduction of the dynamics, yet preserving the reachability of stable states. To that end, we rely on process algebras, a well-established computational technique for the specification and verification of interacting systems. Results: We develop a novel compositional approach to support the logical modelling of interconnected cellular networks. First, we formalize the concept of logical regulatory modules and their composition. Then, we make this framework operational by transposing the composition of logical modules into a process algebra framework. Importantly, the combination of incremental composition, abstraction and minimization using an appropriate equivalence relation (here the safety equivalence) yields huge reductions of the dynamics. We illustrate the potential of this approach with two case-studies: the Segment-Polarity and the Delta-Notch modules. Availability and implementation: GINsim (http://ginsim.org) and CADP (http://cadp.inria.fr) are freely available for academic users. Files needed to reproduce our results are provided at http://compbio.igc.gulbenkian.pt/nmd/node/45. Contact: [email protected] Supplementary information: Supplementary data are available at Bioinformatics online

Abstract Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. Finite state processes (FSP) is a widely used calculus equipped with L tsa , a graphical and user-friendly tool. Language of temporal ordering specification (L otos ) is the only process calculus that has led to an international standard, and is supported by the C adp verification toolbox. We propose a translation of FSP sequential processes into L otos . Since FSP composite processes (i.e., parallel compositions of processes) are hard to encode directly in L otos , they are translated into networks of automata which are another input language accepted by C adp . Hence, it is possible to use jointly L tsa and C adp to validate FSP specifications. Our approach is completely automated by a translator tool.