We study the numerical accuracy of some specific computer programs performing numerical computations. Such a numerical accuracy is expressed in terms of a bound on the difference between the floating-point computations and the corresponding rounding-free computations using mathematical real numbers. We do not only seek to discover such bounds “on paper” but we aim at obtaining computer-assisted formal proofs that these bounds are correct for any possible inputs. The functions we study come from the domain of machine learning: a function computing the logarithm of the sum of exponentials of a sequence, and a similar function related to the computation of mutual information. The bounds obtained are original results, because they are parameterized by assumed error bounds of the underlying implementations of the logarithm and exponential functions. The methodology we follow to conduct our formal proofs is also original, using a combination of the Why3 environment for deductive verification, an original modeling of floating-point computations using unbounded numbers, and the J ^3 environment for proving properties on C source code.

We present our methodology to formally prove properties of VHDL designs by first translating them to Rocq. Because our translation keeps all parameters (a.k.a. generics) uninstantiated, we develop algorithms that check the correctness of given VHDL designs under all parameter valuations. These checks detect whether there are combinatorial loops, missing or multiple signal assignments, wrong integer assignments with respect to specified ranges, array access and assignment errors, and integer overflows for some valuation of the parameters. Once these checks pass, we show how to compute a topological ordering of the signal assignments that is valid for all parameter valuations, and which allows us to translate to simple Rocq functions that capture the functional behaviors of the VHDL designs given as input. We further show to address pipelined circuits and present an application on the verification of a FPU.

We study the numerical accuracy of some specific computer program performing numerical computations. Such a numerical accuracy is expressed in terms of a bound on the difference between the floating-point computation and the corresponding rounding-free computation using mathematical real numbers. We do not only seek to discover such a bound “on paper” but we aim at obtaining computer-assisted formal proofs that this bound is correct for any possible inputs. The function we study comes from the domain of machine learning: a function computing the logarithm of the sum of exponentials of a sequence. The bound obtained is an original result, parameterized by the error bounds of the underlying implementations of the logarithm and exponential functions. The methodology we follow to conduct our formal proofs is also original, using a combination of the Why3 environment for deductive verification, an original modelling of floating-point computations using unbounded numbers, and the J3 environment for proving properties on C source code.

Cyber-physical systems (CPS) are assemblies of networked, heterogeneous, hardware, and software components sensing, evaluating, and actuating a physical environment. This heterogeneity induces complexity that makes CPSs challenging to model correctly. Since CPSs often have critical functions, it is however of utmost importance to formally verify them in order to provide the highest guarantees of safety. Faced with CPS complexity, model abstraction becomes paramount to make verification attainable. To this end, assume/guarantee contracts enable component model abstraction to support a sound, structured, and modular verification process. While abstractions of models by contracts are usually proved sound, none of the related contract frameworks themselves have, to the best of our knowledge, been formally proved correct so far. In this aim, we present the formalization of a generic assume/guarantee contract theory in the proof assistant Coq. We identify and prove theorems that ensure its correctness. Our theory is generic, or parametric, in that it can be instantiated and used with any given logic, in particular hybrid logics, in which highly complex cyber-physical systems can uniformly be described.

Cyber security has been an important issue for control systems, however, there may be a shortage of security experts in the near future. Most of security engineering methods focus only at high-level such as architectures, and do not consider the availability of the control system. In addition, it is often difficult use them without security expertise. In this paper, the author proposed a novel method for solving this problem. The method automatically identifies vulnerabilities in a source code using a formal and static method (type-checking), and fixes them by installing security functions accordingly. Since this approach is entirely automated, it can be seamlessly used by regular engineers, i.e. without security expertise. The authors implemented the method and experimentally investigated its effectiveness on a simple example including the characteristics typical of communicating control systems.

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers. L’archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d’enseignement et de recherche français ou étrangers, des laboratoires publics ou privés. Verifying Temporal Regular properties of Abstractions of Term Rewriting Systems Benoît Boyer, Thomas Genet

Cyber security has been an issue in industrial control systems (ICS) of critical infrastructures. Existing security measures for ordinary enterprise systems are hardly applicable to ICS because they have different requirements. In contrast, whitelisting network monitors attract wide attention as a security measure for ICS that meets the demand for availability during a long lifetime, as well as to exploit the static nature of system configuration. Once defined, the whitelist of allowed packets can detect ever-increasing new attacks without requiring any update. This paper presents a framework for developing reliable and secure whitelisting network monitors for ICS networks such as used in SCADA systems. The proposed approach relies on a model-based development combined with formal verification and proof steps, such that the normal communication model can be verified, the whitelist can be automatically generated from the model and the soundness of the network monitor program can be proven.

Modularity and composability are essential properties to facilitate and scale the design of cyber-physical systems from the specification of hybrid, discrete and continuous, components. Modularity is essential to break down a system model into comprehensible and manageable component specifications. Composability is essential to design a system from component models while preserving their verified properties, expressed as assume-guarantee contracts. In this paper, we address the specification of hybrid system using Platzer's differential dynamic logic (dL). Our contribution is threefold: (1) We define a new composition operator in dL and prove that it is associative and commutative (AC). Prior notions of composition in dL were not associative. (2) We provide a theorem which characterizes necessary conditions to automate the proof that composed components satisfy the composition of their individual contracts, enabling modular and compositional verification. (3) We case-study our AC composition operator by considering the modular and detailed specification of a cruise controller in KeYmaera X, the latest implementation of dL, to demonstrate the proof automation capability of our contribution and exemplify a compositional design methodology.

Complex systems such as systems of systems result from the combination of several components that are organized in a hierarchical manner. One of the main characteristics of those systems is their ability to adapt to new situations by modifying their architecture. Those systems have recently been the subject of a series of works in the software engineering community. Most of those works do not consider quantitative features. The objective of this paper is to propose a modeling language for adaptive systems whose behaviors depend on stochastic features. Our language relies on an extension of stochastic transition systems equipped with (1) an adaptive operator that allows to reason about the probability that a system has to adapt its architecture over time, and (2) dynamic interactions between processes. As a second contribution, we propose a contract-based extension of probabilistic linear temporal logic suited to reason about assumptions and guarantees of such systems. Our work has been implemented in the Plasma-Lab tool developed at Inria. This tool allows us to define stochastic adaptive systems with an extension of the Prism language, and properties with patterns. In addition, Plasma-Lab offers a simulation-based model checking procedure to reason about finite executions of the system. First experiments on a large case study coming from an industrial driven European project give encouraging results.

Invariants generation has been intensively considered as an effective verification method for concurrent systems. However, none of the existing work on the topic strongly exploits the structure of the system and the algebra that defines the interactions between its components. This not only has an impact on the computation time, but also on the scalability of the method. In a series of recent work, we developed an efficient approach for generating invariants for systems described in the BIP component framework. BIP is an expressive modeling formalism including a rich algebra to describe component interactions. Our technique, which focuses on generating Boolean invariants corresponding to a subclass of the conjunctive normal form, was then extended to an incremental one capable of generating global invariants from smaller invariants obtained for sub-systems by exploiting the algebra that describes their interactions. This approach gives a panoply of techniques and libraries to rigorously design potentially complex systems. We also showed that Boolean invariants generated by our methodology correspond to trap of the Petri net induced by the BIP model. Unfortunately, this class of invariants may be too imprecise, and hence leads to discovery of false positive counter examples. The objective of this paper is to propose new techniques dedicated to the computation of linear interactions invariants, i.e., invariants that are described by linear constraints and that relate states of several components in the system. By definition, such new class is incomparable to the one of Boolean invariants, but we will show that it is generally more precise. In addition, we propose an incremental approach that allows to discover and reuse invariants that have already been computed on subparts of the model. Those new techniques have been implemented in DFINDER, a tool for checking deadlock freedom on BIP systems using invariants, and evaluated on several case studies. The experiments show that our approach outperforms classical techniques on a wide range of models.

Exhaustive formal verification for systems of systems (SoS) is impractical and cannot be applied on a large scale. In this paper we propose to use statistical model checking for efficient verification of SoS. We address three relevant aspects for systems of systems: 1) the model of the SoS, which includes stochastic aspects; 2) the formalization of the SoS requirements in the form of contracts; 3) the tool-chain to support statistical model checking for SoS. We adapt the SMC technique for application to heterogeneous SoS. We extend the UPDM/SysML specification language to express the SoS requirements that the implemented strategies over the SoS must satisfy. The requirements are specified with a new contract language specifically designed for SoS, targeting a high-level English- pattern language, but relying on an accurate semantics given by the standard temporal logics. The contracts are verified against the UPDM/SysML specification using the Statistical Model Checker (SMC) PLASMA combined with the simulation engine DESYRE, which integrates heterogeneous behavioral models through the functional mock-up interface (FMI) standard. The tool-chain allows computing an estimation of the satisfiability of the contracts by the SoS. The results help the system architect to trade-off different solutions to guide the evolution of the SoS.

This paper presents some of the results of the first year of DANSE, one of the first EU IP projects dedicated to SoS. Concretely, we offer a tool chain that allows to specify SoS and SoS requirements at high level, and analyse them using powerful toolsets coming from the formal verification area. At the high level, we use UPDM, the system model provided by the british army as well as a new type of contract based on behavioral patterns. At low level, we rely on a powerful simulation toolset combined with recent advances from the area of statistical model checking. The approach has been applied to a case study developed at EADS Innovation Works.

We present PLASMA-lab, a statistical model checking (SMC) library that provides the functionality to create custom statistical model checkers based on arbitrary discrete event modelling languages. PLASMA-lab is written in Java for maximum cross-platform compatibility and has already been incorporated in various performance-critical software and embedded hardware platforms. Users need only implement a few simple methods in a simulator class to take advantage of our efficient SMC algorithms. PLASMA-lab may be instantiated from the command line or from within other software. We have constructed a graphical user interface (GUI) that exposes the functionality of PLASMA-lab and facilitates its use as a standalone application with multiple 'drop-in' modelling languages. The GUI adds the notion of projects and experiments, and implements a simple, practical means of distributing simulations using remote clients.

Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing infinite-state systems in which states are represented by trees and sets of states by tree automata. The central problem is to decide whether a set of bad states belongs to the set of reachable states. An obstacle is that this set is in general neither regular nor computable in finite time. This paper proposes a new CounterExample Guided Abstraction Refinement (CEGAR) algorithm for TRMC. Our approach relies on a new equational-abstraction based completion algorithm to compute a regular overapproximation of the set of reachable states in finite time. This set is represented by ℛ_/E -automata, a new extended tree automaton formalism whose structure can be exploited to detect and remove false positives in an efficient manner. Our approach has been implemented in TimbukCEGAR, a new toolset that is capable of analyzing Java programs by exploiting an elegant translation from the Java byte code to term rewriting systems. Experiments show that TimbukCEGAR outperforms existing CEGAR-based completion algorithms. Contrary to existing TRMC toolsets, the answers provided by TimbukCEGAR are certified by Coq, which means that they are formally proved correct.

In this report, we present functional models for software and hardware components of Time-Triggered Systems on a Chip (TTSoC). These are modeled in the asynchronous component based language BIP. We demonstrate the usability of our components for simulation of software which is developed for the TTSoC. Our software comprises services and an application part. Our approach allows us to simulate and validate aspects of the software system at an early stage in the development process and without the need to have the TTSoC hardware at hand.

The tree automaton completion is an algorithm used for proving safety properties of systems that can be modeled by a term rewriting system. This representation and verification technique works well for proving properties of infinite systems like cryptographic protocols or more recently on Java Bytecode programs. This algorithm computes a tree automaton which represents a (regular) over approximation of the set of reachable terms by rewriting initial terms. This approach is limited by the lack of information about rewriting relation between terms. Actually, terms in relation by rewriting are in the same equivalence class: there are recognized by the same state in the tree automaton.Our objective is to produce an automaton embedding an abstraction of the rewriting relation sufficient to prove temporal properties of the term rewriting system.We propose to extend the algorithm to produce an automaton having more equivalence classes to distinguish a term or a subterm from its successors w.r.t. rewriting. While ground transitions are used to recognize equivalence classes of terms, epsilon-transitions represent the rewriting relation between terms. From the completed automaton, it is possible to automatically build a Kripke structure abstracting the rewriting sequence. States of the Kripke structure are states of the tree automaton and the transition relation is given by the set of epsilon-transitions. States of the Kripke structure are labelled by the set of terms recognized using ground transitions. On this Kripke structure, we define the Regular Linear Temporal Logic (R-LTL) for expressing properties. Such properties can then be checked using standard model checking algorithms. The only difference between LTL and R-LTL is that predicates are replaced by regular sets of acceptable terms.

Tree Regular model checking is the name of a family of techniques for analyzing infinite- state systems in which states are represented by trees and sets of states by tree automata. From the verification point of view, the central problem is to compute the set of reachable states providing a given transition relation. A main obstacle is that this set is in general not computable in a finite time. In this paper, we propose a new CounterExample Guided Abstraction Refinement technique that can be used to check whether a set of state can be reached from the initial set. Contrary to existing techniques, our approach relies on equational abstraction to ease the definition of approximations and on a specific model of tree automata to avoid heavy backward refinement steps.