Increasing design complexity driven by feature and performance requirements and the Time to Market (TTM) constraints force a faster design and validation closure. This in turn enforces novel ways of identifying and debugging behavioral inconsistencies early in the design cycle. Addition of incremental features and timing fixes may alter the legacy design behavior and would inadvertently result in undesirable bugs. The most common method of verifying the correctness of the changed design is to run a dynamic regression test suite before and after the intended changes and compare the results, a method which is not exhaustive. Modern Formal Verification (FV) techniques involving new methods of proving Sequential Hardware Equivalence enabled a new set of solutions for the given problem, with complete coverage guarantee. Formal Equivalence can be applied for proving functional integrity after design changes resulting from a wide variety of reasons, ranging from simple pipeline optimizations to complex logic redistributions. We present here our experience of successfully applying the RTL to RTL (RTL2RTL) Formal Verification across a wide spectrum of problems on a Graphics design. The RTL2RTL FV enabled checking the design sanity in a very short time, thus enabling faster and safer design churn. The techniques presented in this paper are applicable to any complex hardware design.
Interlocking tables are the functional specification defining the routes on which the passage of the train is allowed. Associated with the route, the states and actions of all related signalling equipment are also specified. It is well-known that designing and verifying the interlocking tables are labour intensive, tedious and prone to errors. To assist the verification process and detect errors rapidly, we formally model and analyse the interlocking tables using Coloured Petri Nets (CPNs). Although a large interlocking table can be easily modelled, analysing the model is rather difficult due to the state explosion problem and undesired safe deadlocks. The safe deadlocks are when no train collides but the train traffic cannot proceed any further. For ease of analysis we incorporate automatic route setting and automatic route cancelling functions into the model. These help reducing the number of the deadlocks. We also exploit the new features of CPN Tools; prioritized transitions; inhibitor arcs; and reset arcs. These help reducing the size of the state spaces. We also include a fail safe specification called flank protection into the interlocking model.
Traits allow decomposing programs into smaller parts and mixins are a form of composition that resemble multiple inheritance. Unfortunately, in the presence of traits, programming languages like Scala give up on subtyping relation between objects. In this paper, we present a method to check subtyping between objects based on entailment in separation logic. We implement our method as a domain specific language in Scala and apply it on the Scala standard library. We have verified that 67% of mixins used in the Scala standard library do indeed conform to subtyping between the traits that are used to build them.
High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. The state of the system is not guaranteed to stay within the limits that are admissible for its correct electrical behavior. We show here how to apply a formal method in order to synthesize a correct-by-design control that guarantees that the power converter will always stay within a predefined safe zone of variations for its input parameters. The method is applied in order to synthesize a correct-by-design control for 5-level and 7-level power converters with a flying capacitor topology. We check the validity of our approach by numerical simulations for 5 and 7 levels. We also perform physical experimentations using a prototype built by SATIE laboratory for 5 levels.
Smart systems equipped with emerging pervasive computing technologies enable people with limitations to live in their homes independently. However, lack of guarantees for correctness prevent such system to be widely used. Analysing the system with regard to correctness requirements is a challenging task due to the complexity of the system and its various unpredictable faults. In this work, we propose to use formal methods to analyse pervasive computing (PvC) systems. Firstly, a formal modelling framework is proposed to cover the main characteristics of such systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of deadlocks and conflicts) and specify them as safety and liveness properties. Furthermore, based on the modelling framework, we propose an approach of verifying reasoning rules which are used in the middleware for perceiving the environment and making adaptation decisions. Finally, we demonstrate our ideas using a case study of a smart healthcare system. Experimental results show the usefulness of our approach in exploring system behaviours and revealing system design flaws such as information inconsistency and conflicting reminder services.
This work deals with data analysis issues in an aeronautics context by using a formal framework relying on activity recognition techniques which are applied to the certification and safety analysis processes of Unmanned Aircraft Systems in breakdown situations. In this paper, the behaviour of these systems is modelled, simulated and studied in case of multiple failures using a complex event processing language called chronicles to describe which combinations of events in time may lead to safety breaches, and a C++ chronicle recognition library is used to implement this method.
When programmers want to prove strong program invariants, they are usually faced with a choice between using theorem provers and using traditional programming languages. The former requires them to provide program proofs, which, for many applications, is considered a heavy burden. The latter provides less guarantees and the programmer usually has to write run-time assertions to compensate for the lack of suitable invariants expressible in the type system. We introduce Mezzo, a programming language in the tradition of ML, in which the usual concept of a type is replaced by a more precise notion of a permission. Programs written in Mezzo usually enjoy stronger guarantees than programs written in pure ML. However, because Mezzo is based on a type system, the reasoning requires no user input. In this paper, we illustrate the key concepts of Mezzo, highlighting the static guarantees our language provides.
In a previous work, we have shown how to generate attractor sets of affine hybrid systems using a method of state space decomposition. We show here how to adapt the method to polynomial dynamics systems by approximating them as switched affine systems. We show the practical interest of the method on standard examples of the literature.
The formalism of parametric timed automata provides designers with a formal way to specify and verify real-time concurrent systems where iming requirements are unknown (or parameters). Such models are usually subject to the state space explosion. A popular way to partially reduce the size of the state space is to reduce the number of clock variables. In this work, we present a technique for dynamically eliminating clocks. Experiments using IMITATOR show a diminution of the number of states and of the computation time, and in some cases allow termination of the analysis of models that could not terminate otherwise. More surprisingly, even when the number of clocks remains constant, there is little noticeable overhead in applying the proposed clock elimination.
Traditionally, the focus of specification mechanism has been on improving its ability to cover a wider range of problems more accurately, while the effectiveness of verification is left to the underlying theorem provers. Our work attempts a novel approach, where the focus is on designing good specification mechanisms that can achieve both better expressiveness and better verifiability. Moreover, we shall also highlight a unified specification mechanism that can be used for both verification and inference. Our framework allows preconditions and postconditions to be selectively inferred via a set of uninterpreted relations which are computed using bi-abduction, and modularly synthesized to support concise specification for program codes.
Highly dynamic and complex computing systems are increasingly needed and are relied upon in daily life. One such system is the dynamic network, particularly in communication, in which it has widespread applications, such as: Internet, peer-to-peer networks, mobile networks and wireless networks. Dynamic networks consist of nodes and edges whose operating status may change over time; the edges may be unreliable and operate intermittently. Message-passing in such networks is inherently difficult and reasoning about the behaviour of message-passing algorithms is also difficult and hard to analyse. Their behaviour and correctness are hard to formulate and establish.To undertake formal reasoning about such systems, abstract models are essential in order to separate the general reasoning about message routing and the updating of routing tables from the details of how these are implemented in particular networks.This thesis proposes a new approach to modelling and reasoning about dynamic networks as follows. It develops a series of abstract models which makes it possible to focus on the correctness of routing methods. It models the dynamic network as a ?demonic? process which runs concurrently with routing updates and message-passing, to express dynamic networks as concurrent systems. This allows the use of temporal logic and fairness constraints to reason about dynamic networks. To do so, it introduces a modal logic and formulates concepts of fairness which capture network properties. The correctness of dynamic networks means that under certain conditions, all messages will eventually be delivered. Formulating networks as concurrent systems means can establish the correctness for networks that never cease to change. Modelling at that one level of abstraction means being able to prove the properties of networks independently of the mechanisms in actual networks. Therefore, it provides ?a factorisation? of proofs of correctness for actual dynamic networks. The models are implemented as multi-threaded programs, and then adopted an experimental runtime verification tool called RULER to test whether model instances satisfy the modal correctness for message delivery.
Switched systems are embedded devices widespread in industrial applications such as power electronics and automotive control. They consist of continuous-time dynamical subsystems and a rule that controls the switching between them. Under a suitable control rule, the system can improve its steady-state performance and meet essential properties such as safety and stability in desirable operating zones. We explain that such controller synthesis problems are related to the construction of appropriate invariants of the state space, which approximate the limit sets of the system trajectories. We present a new approach of invariant construction based on a technique of state space decomposition interleaved with forward fixed point computation. The method is illustrated in a case study taken from the field of power electronics. This work is a joint work with Romain Soulat. 1998 ACM Subject Classification D.2.4 Formal methods
Petri nets are a well-known model language for concurrent systems. The unfolding of a Petri net is an acyclic net bisimilar to the original one. Because it is acyclic, it admits simpler decision problems though it is in general larger than the net. In this paper, we revisit the problem of efficiently constructing an unfolding. We propose a new method that avoids computing the concurrency relation and therefore uses less memory than some other methods but still represents a good time-space tradeoff. We implemented the approach and report on experiments.
SystemC is a de-facto industry standard for developing, modelling, and simulating embedded systems. As embedded systems become more and more integrated into many aspects of human lives (e.g., transportation, surveillance systems, ...), failures of embedded systems might cause dangerous hazards to individuals or groups. Guaranteeing safety of such systems makes formal verification crucial. In this paper we present a novel approach for verifying SystemC models with SPIN. Focusing on system-level verification we reuse compiled and executable code from the original model and embed it into the verifier generated by SPIN. In contrast to most other approaches, which require a complete model transformation, in our approach the transformation focuses only on the relevant parts of the model while leaving functional blocks untransformed. Our technique aims at reducing the state vector size managed by the verifier of SPIN, at improving state exploration performance by avoiding unnecessary model transformation steps, and at concentrating on verifying properties that emerge from the composition of multiple functional units.
Hard real time systems are evolving in order to respond to the increasing demand in complex functionalities while taking advantage of newer hardware. Software development for safety critical systems has to comply with strict requirements that will facilitate the certification process. During this process, each part of the system is evaluated, requiring a certain level of assurance in order to provide confidence in the product. In particular there must be a level of confidence that the system behaves deterministically that may be based on functionality, resources and time. The success of system verification depends greatly on the capacity to determine its exact behavior. Nonetheless, hardware evolved in order to maximize the average computation power throughput with little to no regard to the deterministic aspect. Therefore modern architectural features of processors, like pipelines, cache memories and co-processors, make it hard to verify that all the needed properties are respected. The multi-core is furthermore difficult to analyze as the architecture employs mechanisms that compromise strong spatial and temporal partitioning when using shared resources without rigorous access control like shared caches or shared input/outputs. In this paper we identify and analyze the main sources of nondeterminism of the multi-cores with regard to the timing estimation. Precise determination of the worst case execution time is a challenging task even in single-core architectures. The problems are accentuated in the multi-core context mainly due to the resource sharing that can lead to highly complex interactions or to nondeterminism. Most of the units that generate behaviors that are hard to take into account can be deactivated, but it is not always easy to predict the impact on the performance. Nevertheless some of the features cannot be disabled (such as the out of order execution or some nondeterministic crossbar access policies) which leads to the invalidation of the respective platform for applications with high criticality level. We will address the problematic units, propose configuration or architecture guidelines and estimate their impact on the performance and determinism of the system.
The simultaneous-open procedure of the Datagram Congestion Control Protocol (DCCP), RFC 5596, was published in September 2009. Its design aims to overcome DCCP weaknesses when the Server is behind a middle box, such as Network Address Translators or firewalls. The original DCCP specification, RFC 4340, only allows the Client to initiate the call. The call request cannot reach the Server behind the middle box. A widely used solution to address this problem is called the hole punching technique. This technique requires the Server to initiate sending packets. Using Coloured Petri Nets (CPN) this paper models and analyses the DCCP procedure specified in RFC 5596. However, the difficulty is that detailed modelling of the address translation is also required. This causes state space explosion. We alleviate the state explosion using prioritized transitions and the sweep-line technique. Modelling and analysis approaches are discussed in the hope that it is helpful for others who wish to analyse similar protocols. Analysis results are also obtained for the simultaneous-open procedure specified in RFC 5596.
Switched systems are embedded devices widespread in industrial applications such as power electronics and automotive control. They consist of continuous-time dynamical subsystems and a rule that controls the switching between them. Under a suitable control rule, the system can improve its steady-state performance and meet essential properties such as safety and stability in desirable operating zones. We explain that such controller synthesis problems are related to the construction of appropriate invariants of the state space, which approximate the limit sets of the system trajectories. We present a new approach of invariant construction based on a technique of state space decomposition interleaved with forward fixed point computation. The method is illustrated in a case study taken from the field of power electronics.
Smart systems equipped with emerging pervasive computing technologies enable people with limitations to live in their homes independently. However, lack of guarantees for correctness prevent such system to be widely used. Analysing the system with regard to correctness requirements is a challenging task due to the complexity of the system and its various unpredictable faults. In this work, we propose to use formal methods to analyse pervasive computing (PvC) systems. Firstly, a formal modelling framework is proposed to cover the main characteristics of such systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of deadlocks and conflicts) and specify them as safety and liveness properties. Furthermore, based on the modelling framework, we propose an approach of verifying reasoning rules which are used in the middleware for perceiving the environment and making adaptation decisions. Finally, we demonstrate our ideas using a case study of a smart healthcare system. Experimental results show the usefulness of our approach in exploring system behaviours and revealing system design flaws such as information inconsistency and conflicting reminder services.
