Series-parallel (SP) graphs are binary edge-labeled graphs with a designated source and target vertex, built using serial and parallel composition. A set of graphs is recognizable if membership depends only on its image under a homomorphism into a finite algebra. For SP-graphs, and more generally, for graphs of bounded tree-width, recognizability coincides with definability in Counting Monadic Second-Order (CMSO) logic. Despite this strong logical characterization, the conciseness and algorithmic effectiveness of syntactic representations of recognizable sets of SP (and bounded-tree-width) graphs remain poorly understood. Building on previously introduced regular grammars for SP-graphs, we show that recognizable sets admit concise and effective syntactic representations. The main contribution is an improved construction of finite recognizer algebras whose size is singly-exponential in the size of a regular grammar, improving upon the previously known double-exponential bound. As a consequence, the problems of intersection and language inclusion for sets represented by regular grammars are shown to be EXPTIME-complete, thus improving on a previously known 2EXPTIME upper bound.

Abstract We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars in the style of Courcelle. Due to the undecidability of verification problems such as reachability or coverability of a given configuration, in which we count the number of replicas in each local state, we develop two orthogonal verification techniques. We present a counting abstraction able to produce, from a graph grammar describing a parameterized system, a finite set of Petri nets that over-approximate the behaviors of the original system. The counting abstraction is implemented in a prototype tool, evaluated on a non-trivial set of test cases. Moreover, we identify a decidable fragment, for which the coverability problem is in and -hard.

An aggregative composition is a binary operation obeying the principle that the whole is determined by the sum of its parts. The development of graph algebras, on which the theory of formal graph languages is built, relies on aggregative compositions that behave like disjoint union, except for a set of well-marked interface vertices from both sides, that are joined. The same style of composition has been considered in the context of relational structures, that generalize graphs and use constant symbols to label the interface. In this paper, we study a non-aggregative composition operation, called fusion, that joins non-deterministically chosen elements from disjoint structures. The sets of structures obtained by iteratively applying fusion do not always have bounded tree-width, even when starting from a tree-width bounded set. First, we prove that the problem of the existence of a bound on the tree-width of the closure of a given set under fusion is decidable, when the input set is described inductively by a finite hyperedge-replacement (HR) grammar, written using the operations of aggregative composition, forgetting and renaming of constants. Such sets are usually called context-free. Second, assuming that the closure under fusion of a context-free set has bounded tree-width, we show that it is the language of an effectively constructible HR grammar. A possible application of the latter result is the possiblity of checking whether all structures from a non-aggregatively closed set having bounded tree-width satisfy a given monadic second order logic formula.

Regular word grammars are restricted context-free grammars that define all the recognizable languages of words. This paper generalizes regular grammars from words to certain classes of graphs, by defining regular grammars for unordered unranked trees and graphs of tree-width 2 at most. The qualifier "regular" is justified because these grammars define precisely the recognizable (equivalently, CMSO-definable) sets of the respective graph classes. The proof of equivalence between regular and recognizable sets of graphs relies on the effective construction of a recognizer algebra of size doubly-exponential in the size of the grammar. This sets a 2EXPTIME upper bound on the (EXPTIME-hard) problem of inclusion of a context-free language in a regular language, for graphs of tree-width 2 at most. A further syntactic restriction of regular grammars suffices to capture precisely the MSO-definable sets of graphs of tree-width 2 at most, i.e., the sets defined by CMSO formulæ without cardinality constraints. Moreover, we show that MSO-definability coincides with recognizability by algebras having an aperiodic parallel composition semigroup, for each class of graphs defined by a bound on the tree-width.

International audience

International audience

Many industrials consider blockchain as a technology breakthrough for cybersecurity, with use cases ranging from cryptocurrency system to smart contracts, and so forth. While IoT systems employ a lightweight communication protocol between physical objects, blockchain may ensure safe information gathering. Unfortunately, the mixture of both technologies has yet to be formally investigated regarding the consensus algorithm. In this paper, statistical model checking is applied to provide quantitative answers on whether the modeled system satisfies safety and liveness properties expressed in LTL temporal logic.

We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata.

We propose an automated method for computing inductive invariants used to proving deadlock freedom of parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from interaction formulae defining the system architecture. The paper presents the theoretical foundations of the method, including new results for the first order monadic logic and proves its soundness. It also reports on a preliminary experimental evaluation on several textbook examples.

Summary The design of software for networked systems with nodes running an Internet of things operating system faces important challenges due to the heterogeneity of interacting things and the constraints stemming from the often limited amount of available resources. In this context, it is hard to build confidence that a design solution fulfills the application's requirements. This paper introduces a design flow for web service applications of the representational state transfer style that is based on a formal modeling language, the behaviour, interaction, priority (BIP) component framework. The proposed flow applies the principles of separation of concerns in a component‐based design process that supports the modular design and reuse of model artifacts. The BIP tools for state‐space exploration allow verifying qualitative properties for service responsiveness, ie, the timely handling of events. Moreover, essential quantitative properties are validated through statistical model checking of a stochastic BIP model. All properties are preserved in actual implementation by ensuring that the deployed code is consistent with the validated model. We illustrate the design of a representational state transfer sense‐compute‐control application for a Wireless Personal Area Network architecture with nodes running the Contiki operating system. The results validate qualitative and quantitative properties for the system and include the study of error behaviours.

We present a criterion for checking local and global deadlock freedom of finite state systems expressed in BIP: a component-based framework for constructing complex distributed systems. Our criterion is evaluated by model-checking a set of subsystems of the overall large system. If satisfied in small subsystems, it implies deadlock-freedom of the overall system. If not satisfied, then we re-evaluate over larger subsystems, which improves the accuracy of the check. When the subsystem being checked becomes the entire system, our criterion becomes complete for deadlock-freedom. Hence our criterion only fails to decide deadlock freedom because of computational limitations: state-space explosion sets in when the subsystems become too large. Our method thus combines the possibility of fast response together with theoretical completeness. Other criteria for deadlock freedom, in contrast, are incomplete in principle, and so may fail to decide deadlock freedom even if unlimited computational resources are available. Also, our criterion certifies freedom from local deadlock, in which a subsystem is deadlocked while the rest of the system executes. Other criteria only certify freedom from global deadlock. We present experimental results for dining philosophers and for a multi-token-based resource allocation system, which subsumes several data arbiters and schedulers, including Milner’s token-based scheduler.

The design and the implementation of distributed real-time systems has always been a challenging task. A central question being how to efficiently coordinate parallel activities by means of point-to-point communication so as to keep global consistency while meeting timing constraints. In the domain of safety critical applications, system predictability allows to pre-compute optimal scheduling policies. In this paper, we consider a larger class of systems represented as compositions of timed automata subject to multiparty interactions, for which an implementation method for distributed platforms and based on intermediate model transformation already exists. To improve this approach, we developed specific static analysis techniques that, combined with local and global knowledge of the system, checks particular conditions that enables to decrease the number of messages exchanged in the system for executing each interaction, as well as to remove unnecessary scheduling overhead in some cases.

Abstract This paper addresses the monitoring of logic-independent linear-time user-provided properties in multi-threaded component-based systems. We consider intrinsically independent components that can be executed concurrently with a centralized coordination for multiparty interactions. In this context, the problem that arises is that a global state of the system is not available to the monitor. A naive solution to this problem would be to plug in a monitor which would force the system to synchronize in order to obtain the sequence of global states at runtime. Such a solution would defeat the whole purpose of having concurrent components. Instead, we reconstruct on-the-fly the global states by accumulating the partial states traversed by the system at runtime. We define transformations of components that preserve their semantics and concurrency and, at the same time, allow to monitor global-state properties. Moreover, we present RVMT-BIP, a prototype tool implementing the transformations for monitoring multi-threaded systems described in the Behavior, Interaction, Priority (BIP) framework, an expressive framework for the formal construction of heterogeneous systems. Our experiments on several multi-threaded BIP systems show that RVMT-BIP induces a cheap runtime overhead.

Building abstract system-level models that faithfully capture performance and functional behavior for embedded systems design is challenging. Unlike functional aspects, performance details are rarely available during the early design phases, and no clear method is known to characterize them. Moreover, once such models are built, they are inherently complex as they mix software models, hardware constraints, and environment abstractions. Their analysis by using traditional performance evaluation methods is reaching the limit. In this article, we present a systematic approach for building stochastic abstract performance models using statistical inference and model calibration, and we propose statistical model checking as a scalable performance evaluation technique for them.

The real-time system design targeting multiprocessor platforms leads to two important complications in real-time scheduling. First, to ensure deterministic processing by communicating tasks the scheduling has to consider precedence constraints. The second complication factor is mixed criticality, i.e., Integration upon a single platform of various subsystems where some are safety-critical (e.g., Car braking system) and the others are not (e.g., Car digital radio). Therefore we motivate and study the multiprocessor scheduling problem of a finite set of precedence-related mixed criticality jobs. This problem, to our knowledge, has never been studied if not under very specific assumptions. The main contribution of our work is an algorithm that, given a global fixed-priority assignment for jobs, can modify it in order to improve its schedulability for mixed-criticality setting. Our experiments show an increase of schedulable instances up to a maximum of 30% if compared to classical solutions for this category of scheduling problems.

Performance and functional correctness are key for successful design of modern embedded systems. Both aspects must be considered early in the design process to enable founded decision making towards final implementation. Nonetheless, building abstract system-level models that faithfully capture performance information along to functional behavior is a challenging task. In contrast to functional aspects, performance details are rarely available during early design phases and no clear method is known to characterize them. Moreover, once such system-level models are built they are inherently complex as they usually mix software models, hardware architecture constraints and environment abstractions. Their analysis by using traditional performance evaluation methods is reaching the limits and the need for more scalable and accurate techniques is becoming urgent. In this paper, we introduce a systematic method for building stochastic abstract performance models using statistical inference and model calibration and we propose statistical model checking as performance evaluation technique upon the obtained models. We experimented our method on a real-life case study and we were able to verify different timing properties.

Using the advances of the modern microelectronics technology, the safety-critical systems, such as avionics, can reduce their costs by integrating multiple tasks on one device. This makes such systems essentially mixed-critical, as this brings together different tasks whose safety assurance requirements may differ significantly. In the context of mixed-critical scheduling theory, we studied the dual criticality problem of scheduling a finite set of hard real-time jobs. In this work we propose an algorithm which is proved to dominate OCBP, a state-of-the art algorithm for this problem that is optimal over fixed job priority algorithms. We show through empirical studies that our algorithm can reduce the set of non-schedulable instances by a factor of two or, under certain assumptions, by a factor of four, when compared to OCBP.

This paper surveys well-established/recent tools and techniques developed for the design of rigorous embedded systems. We will first survey UPPAAL and MODEST, two tools capable of dealing with both timed and stochastic aspects. Then, we will overview the BIP framework for modular design and code generation. Finally, model-based testing will be discussed.

Design correctness and performance are major issues which are usually considered separately, and with different emphasis, by traditional system design flows. In this paper we show that one can meaningfully connect and benefit from the advantages of two design frameworks, with different design goals. We consider BIP for high-level rigorous design and correct-by-construction implementation, and metroII, for low-level platform-based design and performance evaluation.

Programable logic controllers (PLCs) are complex cyber-physical systems which are widely used in industry. This paper shows the modeling and validation work of a typical PLC control system using the Behavior-Interaction-Priority(BIP) component framework. The gate control system based on PLC is a real industry application. We design general system architecture for this kind of device control system. The control software and hardware of environment are all modeled as BIP components. Their interactions are described by BIP connectors. System requirements are formalized as monitors. Simulation is applied on the system model. We found a couple of design errors in simulation, which help us to improve the dependability of the original systems.

In this paper, we introduce a novel model-based approach for constructing correct distributed implementation of component-based models constrained by priorities. We argue that model-based methods are especially of interest in the context of distributed embedded system due to their inherent complexity. Our three-phase method's input is a model specified in terms of a set of behavioural components that interact through a set of high-level synchronization primitives (e.g., rendezvous and broadcasts) and priority rules for scheduling purposes. Our technique, first, transforms the input model into a model that has no priorities. Then, it transforms the deprioritized model into another model that resolves distributed conflicts by incorporating a solution to the committee coordination problem. Finally, it generates distributed code using asynchronous point-to-point send/receive primitives. All transformations preserve the properties of their input model by ensuring observational equivalence. The transformations are implemented and our experiments validate their effectiveness.

A grand challenge in complex embedded systems design is developing methods and tools for modeling and analyzing the behavior of an application software running on multicore or distributed platforms. We propose a rigorous method and a tool chain that allows to obtain a faithful model representing the behavior of a mixed hardware/software system from a model of its application software and a model of its underlying hardware architecture. The system model can be simulated and analyzed for validation of both functional and extra-functional properties. The tool chain uses DOL (Distributed Operation Layer [1]) as the frontend for specifying the application software and hardware architecture, and BIP (Behavior Interaction Priority [2]) as the modeling and analysis framework. It is illustrated through the construction of system models of MJPEG and MPEG2 decoder applications running on MPARM, a multicore architecture.

This paper introduces a theory of fault recovery for component-based models. In our framework, a model is specified in terms of a set of atomic components that are incrementally composed and synchronized by a set of glue operators. We define what it means for such models to provide a recovery mechanism, so that the model converges to its normal behavior in the presence of faults. We identify corrector (atomic or composite) components whose presence in a model is essential to guarantee recovery after the occurrence of faults. We also formalize component-based models that effectively separate recovery from functional concerns.

Although distributed systems are widely used nowadays, their implementation and deployment is still a time-consuming, error-prone, and hardly predictive task. In this paper, we propose a methodology for producing automatically efficient and correct-by-construction distributed implementations by starting from a high-level model of the application software in BIP. BIP (Behavior, Interaction, Priority) is a component-based framework with formal semantics that rely on multi-party interactions for synchronizing components. Our methodology transforms arbitrary BIP models into Send/Receive BIP models, directly implementable on distributed execution platforms. The transformation consists of (1) breaking atomicity of actions in atomic components by replacing strong synchronizations with asynchronous Send/Receive interactions; (2) inserting several distributed controllers that coordinate execution of interactions according to a user-defined partition, and (3) augmenting the model with a distributed algorithm for handling conflicts between controllers preserving observational equivalence to the initial models. Currently, it is possible to generate from Send/Receive models stand-alone C++ implementations using either TCP sockets for conventional communication, or MPI implementation, for deployment on multi-core platforms. This method is fully implemented. We report concrete results obtained under different scenarios.

Behavior, Interaction, Priorities (BIP) is a component framework for constructing systems from a set of atomic components by using two kinds of composition operators: interactions and priorities. In this paper, we present a method that transforms the interactions of a component-based program in BIP and generates a functionally equivalent program. The method is based on the successive application of three types of source-to-source transformations: flattening of components, flattening of connectors, and composition of atomic components. We show that the system of the transformations is confluent and terminates. By exhaustive application of the transformations, any BIP component can be transformed into an equivalent monolithic component. From this component, efficient standalone C++ code can be generated. The method combines advantages of component-based description such as clarity, incremental construction, and reasoning with the possibility to generate efficient monolithic code. It has been integrated in the design methodology for BIP and it has been successfully applied to two non trivial examples described in this paper.

We provide a verification technique for a class of programs working on integer arrays of finite, but not a priori bounded length. We use the logic of integer arrays SIL [13] to specify pre- and post-conditions of programs and their parts. Effects of non-looping parts of code are computed syntactically on the level of SIL. Loop pre-conditions derived during the computation in SIL are converted into counter automata (CA). Loops are automatically translated—purely on the syntactical level—to transducers. Pre-condition CA and transducers are composed, and the composition over-approximated by flat automata with difference bound constraints, which are next converted back into SIL formulae, thus inferring post-conditions of the loops. Finally, validity of post-conditions specified by the user in SIL may be checked as entailment is decidable for SIL.

International audience

We develop and implement a methodology for automatic abstraction of systems defined as networks of timed components modeled by timed automata. The abstraction technique yields an abstract model with much less clocks and states which over-approximate the timed behavior of the concrete system. Using this technique we can analyze timed system of size beyond the capabilities of contemporary analysis tools for timed automata.

In this paper we study the reachability problem for parametric flat counter automata, in relation with the satisfiability problem of three fragments of integer arithmetic. The equivalence between non-parametric flat counter automata and Presburger arithmetic has been established previously by Comon and Jurski. We simplify their proof by introducing finite state automata defined over alphabets of a special kind of graphs (zigzags). This framework allows one to express also the reachability problem for parametric automata with one control loop as the satisfiability of a 1-parametric linear Diophantine systems. The latter problem is shown to be decidable, using a number-theoretic argument. In general, the reachability problem for parametric flat counter automata with more than one loops is shown to be undecidable, by reduction from Hilbert's Tenth Problem. Finally, we study the relation between flat counter automata, integer arithmetic, and another important class of computational devices, namely the 2-way reversal bounded counter machines.

We present a methodology for modeling heterogeneous real-time components. Components are obtained as the superposition of three layers: behavior, specified as a set of transitions; Interactions between transitions of the behavior; Priorities, used to choose amongst possible interactions. A parameterized binary composition operator is used to compose components layer by layer. We present the BIP language for the description and composition of layered components as well as associated tools for executing and analyzing components on a dedicated platform. The language provides a powerful mechanism for structuring interactions involving rendezvous and broadcast. We show that synchronous and timed systems are particular classes of components. Finally, we provide examples and compare the BIP framework to existing ones for heterogeneous component-based modeling

In this paper we address the following problem: given an acyclic program scheme with if-then-else control structures, together with the duration of each procedure, and given an architecture consisting of n identical processors, compute offline a scheduling policy that guarantees minimal execution time (in the worst-case) for the entire program on this architecture. Since this is a problem of scheduling under uncertainty (the results of the branching decisions are not known in advance) it cannot be solved in a satisfactory manner using static or fixed priority schedulers but rather requires a state-dependent scheduling strategy. We use timed automata technology to derive such strategies using algorithms for finding shortest paths on game graphs.

Pioneering work has been done by Jonkers [18] to define a semantics of pointer manipulating programs that is abstract in the sense of ignoring low-level aspects such as dangling pointers and garbage objects. We explore the principles of such storeless semantics from a logical point of view, first defining a simple logic to completely characterize heap structures up to isomorphism. Second, we extend this language to a full-blown alias logic (AL) that allows to express regular properties of unbounded heap structures. Along the development, we present an operational storeless semantics and give sound and complete total correctness axioms for deterministic programs in the form of Hoare triples, using AL.

This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools can cover by itself the whole validation process. The IF environment was built upon an expressive intermediate language and allows to connect several validation tools, providing most of the advanced techniques currently available. The results obtained on several large case-studies, including telecommunication protocols and embedded software systems, confirm the practical interest of this approach.