Assuring quality for cyber-physical systems has been a significant concern, leading to various proposed solutions. Faults in cyber-physical systems lead to security and safety issues in communication and operation, respectively. To prevent harm, verification and validation methodologies are applied during development. However, there might be no guarantee that the final deployed system is fault-free, i.e., a residual risk always remains. This paper focuses on involved risks, identifies their sources, and discusses methods for risk reduction in cyber-physical systems. For this purpose, a holistic approach to risk reduction in cyber-physical systems is utilized. Further, different stages of system development and operation are explained, and methodologies for finding defects and evaluating risks are discussed. Finally, concepts and methods using an industrial battery management system are presented. Specifically, the benefits of using formal methods to reduce risks in the context of autonomous driving and ADAS functionality are illustrated.

SoC architectures are complex and notoriously hard to verify. Current industrial practice is still mainly based on testing, with the recent standard PSS easing the generation of system-level tests. In this paper, we suggest to formally express the behavior of a PSS model as a composition of communicating labeled transition systems. This improves the PSS methodology in two ways. First, it becomes possible to formally verify temporal logic properties of the model and increase the confidence in the model and the generated tests. Second, conformance testing techniques improve the coverage of the generated tests.

Simulation, a common practice to evaluate au-tonomous vehicles, requires to specify realistic scenarios, in par-ticular critical ones, occurring rarely and potentially dangerous to reproduce on the road. Such scenarios may be either generated randomly, or specified manually. Randomly generating scenarios is easy, but their relevance might be difficult to assess. Manually specified scenarios can focus on a given feature, but their design might be difficult and time-consuming, especially to achieve satisfactory coverage. In this work, we propose an automatic approach to generate a large number of relevant critical scenarios for autonomous driving simulators. The approach is based on the generation of behavioral conformance tests from a formal model (specifying the ground truth configuration with the range of vehicle behaviors) and a test purpose (specifying the critical feature to focus on). The obtained abstract test cases cover, by construction, all possible executions exercising a given feature, and can be automatically translated into the inputs of autonomous driving simulators. We illustrate our approach by generating thousands of behavior trees for the CARLA simulator for several realistic configurations.

Consumer Internet of Things (IoT) applications are largely built through end-user programming in the form of event-action rules. Although end-user tools help simplify the building of IoT applications to a large extent, there are still challenges in developing expressive applications in a simple yet correct fashion. In this context, we propose a formal development framework based on the Web of Things specification. An application is defined using a composition language that allows users to compose the basic event-action rules to express complex scenarios. It is transformed into a formal specification that serves as the input for formal analysis, where the application is checked for functional and quantitative properties at design time using model checking techniques. Once the application is validated, it can be deployed and the rules are executed following the composition language semantics. We have implemented these proposals in a tool built on top of the Mozilla WebThings platform. The steps from design to deployment were validated on real-world applications.

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.

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

Reuse and composition are increasingly advocated and put into practice in modern software engineering. However, the software entities that are to be reused to build an application, e.g., services, have seldom been developed to integrate and to cope with the application requirements. As a consequence, they present mismatch, which directly hampers their reusability and the possibility of composing them. Software Adaptation has become a hot topic as a nonintrusive solution to work mismatch out using corrective pieces named adaptors. However, adaptation is a complex issue, especially when behavioral interfaces, or conversations, are taken into account. In this paper, we present state-of-the-art techniques to generate adaptors given the description of reused entities' conversations and an abstract specification of the way mismatch can be solved. We use a process algebra to encode the adaptation problem, and propose on-the-fly exploration and reduction techniques to compute adaptor protocols. Our approach follows the model-driven engineering paradigm, applied to service-oriented computing as a representative field of composition-based software engineering. We take service description languages as inputs of the adaptation process and we implement adaptors as centralized service compositions, i.e., orchestrations. Our approach is completely tool supported.

BACKGROUND: The study of biological networks has led to the development of increasingly large and detailed models. Computer tools are essential for the simulation of the dynamical behavior of the networks from the model. However, as the size of the models grows, it becomes infeasible to manually verify the predictions against experimental data or identify interesting features in a large number of simulation traces. Formal verification based on temporal logic and model checking provides promising methods to automate and scale the analysis of the models. However, a framework that tightly integrates modeling and simulation tools with model checkers is currently missing, on both the conceptual and the implementational level. RESULTS: We have developed a generic and modular web service, based on a service-oriented architecture, for integrating the modeling and formal verification of genetic regulatory networks. The architecture has been implemented in the context of the qualitative modeling and simulation tool GNA and the model checkers NUSMV and CADP. GNA has been extended with a verification module for the specification and checking of biological properties. The verification module also allows the display and visual inspection of the verification results. CONCLUSIONS: The practical use of the proposed web service is illustrated by means of a scenario involving the analysis of a qualitative model of the carbon starvation response in E. coli. The service-oriented architecture allows modelers to define the model and proceed with the specification and formal verification of the biological properties by means of a unified graphical user interface. This guarantees a transparent access to formal verification technology for modelers of genetic regulatory networks.

Formal verification based on model checking provides a powerful technology to query qualitative models of dynamical systems. The application of model-checking approaches is hampered, however, by the difficulty for non-expert users to formulate appropriate questions in temporal logic. In order to deal with this problem, we propose the use of patterns, that is, high-level query templates capturing recurring questions which can be automatically translated to temporal logic. We develop a set of patterns for the analysis of qualitative models of genetic regulatory networks, which are sufficiently generic though to be useful in other application domains. The applicability of the patterns has been investigated by the analysis of a model of the network of global regulators controlling the carbon starvation response in Escherichia coli.

Equivalence checking is a classical verification method determining if a finite-state concurrent system (protocol) satisfies its desired external behaviour (service) by comparing their underlying labeled transition systems (LTSs) modulo an appropriate equivalence relation. Local (or on-the- fly) equivalence checking explores the synchronous product of the LTSs incrementally, allowing an efficient detection of errors in complex systems. In this paper, we consider the technique based on translating the equivalence checking problem in terms of the local resolution of a Boolean equation system (BES). We propose two enhancements of this technique in the case of equivalent LTSs: a new, faster BES encoding of weak equivalence relations, and a new local BES resolution algorithm with a good average complexity. These enhancements were incorporated into the BISIMULATOR 2.0 equivalence checker of the CADP toolbox, and led to significant performance improvements.

Software adaptation has been proposed as a solution to mismatch between components through the generation of software pieces called adaptors. We propose a new behavioral adaptation approach for the generation of adaptor protocols. Compared to related work, it is fully automated and addresses the adaptor computation complexity thanks to process algebra encodings and on-the-fly techniques.

On-the-fly verification of concurrent finite-state systems consists in constructing and analysing their underlying state spaces in a demand-driven way. This technique is able to detect errors effectively in large systems; however, its performance can still be increased by reducing the state spaces incrementally in a way compatible with the verification problem. In this paper, we propose algorithms for three on-the-fly reductions of Labeled Transition Systems (LTSs), which preserve weak equivalence relations: Τ-compression (collapsing of strongly connected components made of Τ-transitions), Τ-closure (transitive reflexive closure over Τ-transitions), and Τ-confluence (a form of partial order reduction). Each algorithm is described as a reductor module taking as input the successor function of an LTS and returning the successor function of the reduced LTS. The three reductors were implemented within the CADP toolbox using the generic OPEN/CÆSAR environment, which makes them directly available for any on-the-fly verification tool connected to OPEN/CÆSAR and compatible with the underlying reduction. Our experiments show that these reductors can improve significantly the performance of on-the-fly LTS generation, model checking, and equivalence checking.