Skip to main content



Invited Papers

From Software to Hardware and Back

One of the techniques for the formal design of embedded systems is – or should be – Behavioral Synthesis. Among its many advantages, one can quote easier testing and more complete architecture exploration.
Paul Feautrier

Of Elections and Electrons

Digital voting technologies are currently very topical and hotly debated, especially in the US with a presidential election looming. It is essential that voting systems are both trustworthy and trusted. Various schemes and technologies have been proposed, and indeed deployed, that take drastically different approaches to achieving assurance. At one end of the spectrum, we have approaches that claim to achieve assurance through system verification and testing. At the other end, we have the run-time monitoring school. Another way to characterize this dichotomy is to observe that the former approach seeks to verify the electoral system, the latter seeks to verify an actual election.
Peter Y. Ryan

Regular Papers

Formal Verification of an Avionics Sensor Voter Using SCADE

Redundancy management is widely utilized in mission critical digital flight control systems. This study focuses on the use of SCADE (Safety Critical Application Development Environment) and its formal verification component, the Design Verifier, to assess the design correctness of a sensor voter algorithm used for management of three redundant sensors. The sensor voter algorithm is representative of embedded software used in many aircraft today. The algorithm, captured as a Simulink diagram, takes input from three sensors and computes an output signal and a hardware flag indicating correctness of the output. This study is part of an overall effort to compare several model checking tools to the same problem. SCADE is used to analyze the voter’s correctness in this part of the study. Since synthesis of a correct environment for analysis of the voter’s normal and off-normal behavior is a key factor when applying formal verification tools, this paper is focused on 1) the different approaches used for modeling the voter’s environment and 2) the strengths and shortcomings of such approaches when applied to the problem under investigation.
Samar Dajani-Brown, Darren Cofer, Amar Bouali

Mixed Delay and Threshold Voters in Critical Real-Time Systems

This paper addresses the question of extending the usual approximation and sampling theory of continuous signals and systems to those encompassing discontinuities, such as found in modern complex control systems (mode switches for instance). We provide a topological framework derived from the Skorokhod distance to deal with those cases in a uniform manner. We show how this theoretical framework can be used for voting on hybrid signals in critical real-time systems.
Chiheb Kossentini, Paul Caspi

Towards a Methodological Approach to Specification and Analysis of Dependable Automation Systems

The paper discusses a constructive approach to the temporal logic specification and analysis of dependability requirements of automation systems. The work is based on TRIO formal method, which supports a declarative temporal logic language with a linear notion of time, and makes use of UML class diagrams to describe the automation system. The general concepts presented for the automation system domain are here instantiated on a case study application taken from the energy distribution field.
Simona Bernardi, Susanna Donatelli, Giovanna Dondossola

On Two-Sided Approximate Model-Checking: Problem Formulation and Solution via Finite Topologies

We give a general formulation of approximate model-checking, in which both under- and over-approximations are propagated to give two-sided approximations of the denotation set of an arbitrarily complex formula. As our specification language, we use the modalμ-calculus, since it subsumes standard linear and branching temporal logics over transition systems like LTL, CTL and CTL  ⋆ . We give a general construction of a topological finite approximation scheme for a Kripke model from a state-space discretization via an A/D-map and its induced finite topology. We further show that under natural coherence conditions, any finite approximation scheme can be refined by a topological one.
Jennifer M. Davoren, Thomas Moor, R. P. Goré, Vaughan Coulthard, Anil Nerode

On Timed Automata with Input-Determined Guards

We consider a general notion of timed automata with input-determined guards and show that they admit a robust logical framework along the lines of [6], in terms of a monadic second order logic characterisation and an expressively complete timed temporal logic. We then generalize these automata using the notion of recursive operators introduced by Henzinger, Raskin, and Schobbens [10], and show that they admit a similar logical framework. These results hold in the “pointwise” semantics. We finally use this framework to show that the real-time logic MITL of Alur et al [2] is expressively complete with respect to an MSO corresponding to an appropriate set of input-determined operators.
Deepak D’Souza, Nicolas Tabareau

Decomposing Verification of Timed I/O Automata

This paper presents assume-guarantee style substitutivity results for the recently published timed I/O automaton modeling framework. These results are useful for decomposing verification of systems where the implementation and the specification are represented as timed I/O automata. We first present a theorem that is applicable in verification tasks in which system specifications express safety properties. This theorem has an interesting corollary that involves the use of auxiliary automata in simplifying the proof obligations. We then derive a new result that shows how the same technique can be applied to the case where system specifications express liveness properties.
Dilsun Kırlı Kaynar, Nancy Lynch

Symbolic Model Checking for Simply-Timed Systems

We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).
Nicolas Markey, Philippe Schnoebelen

Robustness and Implementability of Timed Automata

In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by Δ to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter Δ for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a Δ. We show that this question is closely related to a notion of robustness for timed automata defined in [Pur98] and prove that the implementability problem is decidable.
Martin De Wulf, Laurent Doyen, Nicolas Markey, Jean-François Raskin

Real-Time Testing with Timed Automata Testers and Coverage Criteria

In previous work, we have proposed a framework for black-box conformance testing of real-time systems based on timed automata specifications and two types of tests: analog-clock or digital-clock. Our algorithm to generate analog-clock tests is based on an on-the-fly determinization of the specification automaton during the execution of the test, which in turn relies on reachability computations. The latter can sometimes be costly, thus problematic, since the tester must quickly react to the actions of the system under test. In this paper, we provide techniques which allow analog-clock testers to be represented as deterministic timed automata, thus minimizing the reaction time to a simple state jump. We also provide a method for (statically) generating a suite of digital-clock tests which covers the specification with respect to a number of criteria: location, edge or state coverage. This can dramatically reduce the number of generated tests, as can be evidenced on a small example.
Moez Krichen, Stavros Tripakis

Monitoring Temporal Properties of Continuous Signals

In this paper we introduce a variant of temporal logic tailored for specifying desired properties of continuous signals. The logic is based on a bounded subset of the real-time logic mitl, augmented with a static mapping from continuous domains into propositions. From formulae in this logic we create automatically property monitors that can check whether a given signal of bounded length and finite variability satisfies the property. A prototype implementation of this procedure was used to check properties of simulation traces generated by Matlab/Simulink.
Oded Maler, Dejan Nickovic

A Unified Fault-Tolerance Protocol

Davies and Wakerly show that Byzantine fault tolerance can be achieved by a cascade of broadcasts and middle value select functions. We present an extension of the Davies and Wakerly protocol, the unified protocol, and its proof of correctness. We prove that it satisfies validity and agreement properties for communication of exact values. We then introduce bounded communication error into the model. Inexact communication is inherent for clock synchronization protocols. We prove that validity and agreement properties hold for inexact communication, and that exact communication is a special case. As a running example, we illustrate the unified protocol using the SPIDER family of fault-tolerant architectures. In particular we demonstrate that the SPIDER interactive consistency, distributed diagnosis, and clock synchronization protocols are instances of the unified protocol.
Paul Miner, Alfons Geser, Lee Pike, Jeffrey Maddalon

Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications

The fault tolerance theories by Arora and Kulkarni [3] and by Jhumka et al. [8] view a fault-tolerant program as the composition of a fault-intolerant program with fault tolerance components called detectors and correctors. At their core, the theories assume that the correctness specifications under consideration are fusion closed. In general, fusion closure of specifications can be achieved by adding history variables. However, the addition of history variables causes an exponential growth of the state space of the program, causing addition of fault tolerance to be expensive. To redress this problem, we present a method which can be used to add history information to a program in a way that significantly reduces the number of additional states. Hence, automated methods that add fault tolerance can be efficiently applied in environments where specifications are not necessarily fusion closed.
Felix C. Gärtner, Arshad Jhumka

Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol Using Calendar Automata

We discuss the modeling and verification of real-time systems using the SAL model checker. A new modeling framework based on event calendars enables dense timed systems to be described without relying on continuously varying clocks. We present verification techniques that rely on induction and abstraction, and show how these techniques are efficiently supported by the SAL symbolic model-checking tools. The modeling and verification method is applied to the fault-tolerant real-time startup protocol used in the Timed Triggered Architecture.
Bruno Dutertre, Maria Sorea

Static Fault-Tolerant Real-Time Scheduling with “Pseudo-topological” Orders

We give a graph-theoretical model for off-line fault-tolerant scheduling of dataflow algorithms onto multiprocessor architectures with distributed memory. Our framework allows the modeling of both processor and communication channel failures of the “fail silent” type (either transient or permanent), and failure masking is achieved by replicating operations and data communications. We show that, in general, the graph representing a fault-tolerant scheduling may have circuits; hence, the classical computation of starting and ending times of the operations and communications, based upon a topological order, is inapplicable. We thus provide a notion of “pseudo-topological order” that permits the computation of the starting and ending times even in the case of cyclic graphs. We also derive algorithms for computing the timeouts that are used for failure detection.
Cătălin Dima, Alain Girault, Yves Sorel

The Influence of Durational Actions on Time Equivalences

The hierarchy of untimed equivalences is well understood for action-based systems. This is not the case for timed systems, where it is, for example, possible to detect concurrency by single timed action execution. To clarify the connection between equivalences in timed systems, a timed version of configuration structures is introduced together with timed equivalence notions adapted from untimed equivalences. There actions (events) have an occurrence time and a duration. The result of this paper is that all timed versions of the equivalences from [15] have the same relative discriminating power as in the untimed case, except that interleaving and step (for trace and bisimulation) equivalences coincide if systems are considered where every action must have a positive duration.
Harald Fecher

Bounded Model Checking for Region Automata

For successful software verification, model checkers must be capable of handling a large number of program variables. Traditional, BDD-based model checking is deficient in this regard, but bounded model checking (BMC) shows some promise. However, unlike traditional model checking, for which time systems have been thoroughly researched, BMC is less capable of modeling timing behavior – an essential task for verifying many types of software. Here we describe a new bounded model checker we have named xBMC, which we believe solves the reachability problem of dense-time systems. In xBMC, regions and transition relations are represented as Boolean formulae using discrete interpretations. In an experiment using well- developed model checkers to verify Fischer’s protocol, xBMC outperformed both traditional (Kronos [8], Uppaal [16], and Red [26]) and bounded (SAL [21]) model checkers by being able to verify up to 22 processes, followed by Red with 15 processes. Therefore, although xBMC is less efficient in guaranteeing system correctness, it provides an effective and practical method for timing behavior verification of large systems.
Fang Yu, Bow-Yaw Wang, Yao-Wen Huang

Some Progress in Satisfiability Checking for Difference Logic

In this paper we report a new SAT solver for difference logic, a propositional logic enriched with timing constraints. The main novelty of our solver is a tighter integration of the incremental analysis of numerical conflicts with the process of Boolean conflict analysis. This and other improvements lead to significant performance gains for some classes of problems.
Scott Cotton, Eugene Asarin, Oded Maler, Peter Niebert

Model-Checking for Weighted Timed Automata

We study the model-checking problem for weighted timed automata and the weighted CTL logic by the bisimulation approach. Weighted timed automata are timed automata extended with costs on both edges and locations. When the costs act as stopwatches, we get stopwatch automata with the restriction that the stopwatches cannot be reset nor tested. The weighted CTL logic is an extension of TCTL that allow to reset and test the cost variables. Our main results are (i) the undecidability of the proposed model-checking problem for discrete and dense time, (ii) its PSpace-Completeness in the discrete case for a slight restriction of the logic, (iii) the precise frontier between finite and infinite bisimulations in the dense case for the subclass of stopwatch automata.
Thomas Brihaye, Véronique Bruyère, Jean-François Raskin

Symbolic Model Checking for Probabilistic Timed Automata

Probabilistic timed automata are an extension of timed automata with discrete probability distributions, and can be used to model timed randomized protocols or fault-tolerant systems. We present symbolic model-checking algorithms for verifying probabilistic timed automata against properties of PTCTL (Probabilistic Timed Computation Tree Logic). The algorithms operate on zones, which are sets of valuations of the probabilistic timed automaton’s clocks, and therefore avoid an explicit construction of the state space. Furthermore, the algorithms are restricted to system behaviours which guarantee the divergence of time with probability 1. We report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.
Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, Fuzhi Wang

Structured Modeling of Concurrent Stochastic Hybrid Systems

We propose a modeling language for structured specification of interacting components with both hybrid and stochastic dynamics. The behavior of a stochastic hybrid agent is described using a hybrid automaton whose dynamics is specified by stochastic differential equations and probabilistic jumps. Stochastic hybrid agents interact with other agents using shared variables. The operations of parallel composition, instantiation and hiding are defined to allow hierarchical descriptions of complex agents. We report on a stochastic extension of the modeling environment Charon for hybrid systems, a simulation tool, and case studies using the tool.
Mikhail Bernadsky, Raman Sharykin, Rajeev Alur

Computing Schedules for Multithreaded Real-Time Programs Using Geometry

We describe a novel technique for computing efficient schedules for multi-threaded real-time programs. The technique makes use of abstractions which are constructed by embedding the model of the program in a geometric space and then constructing a decomposition of this space. This embedding uses the model of PV diagrams. We introduce a timed version for PV programs and diagrams, which allows us to define the worst-case response time of the schedules, and then to use the geometric abstractions for computing efficient schedules.
Philippe Gerner, Thao Dang

Forward Reachability Analysis of Timed Petri Nets

We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets, by performing symbolic forward reachability analysis. We introduce a formalism, called region generators for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions, and provide exact abstractions of sets of reachable states with respect to safety properties. We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples. We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer’s protocol and a producer-consumer protocol. We also used the tool to extract finite-state abstractions of these protocols.
Parosh Aziz Abdulla, Johann Deneux, Pritha Mahata, Aletta Nylén

Lazy Approximation for Dense Real-Time Systems

We propose an effective and complete method for verifying safety and liveness properties of timed systems, which is based on predicate abstraction for computing finite abstractions of timed automata and TCTL formulas, finite-state CTL model checking, and successive refinement of finite-state abstractions. Starting with some coarse abstraction of the given timed automaton and the TCTL formula we define a finite sequence of refined abstractions that converges to the region graph of the real-time system. In each step, new abstraction predicates are selected nondeterministically from a finite, predetermined basis of abstraction predicates. Symbolic counterexamples from failed model-checking attempts are used to heuristically choose a small set of new abstraction predicates for incrementally refining the current abstraction. Without sacrificing completeness, this algorithm usually does not require computing the complete region graph to decide model-checking problems. Abstraction refinement terminates quickly, as a multitude of spurious counterexamples is eliminated in every refinement step through the use of symbolic counterexamples for TCTL.
Maria Sorea

Learning of Event-Recording Automata

We extend Angluin’s algorithm for on-line learning of regular languages to the setting of timed systems. We consider systems that can be described by a class of deterministic event-recording automata. We present two algorithms that learn a description by asking a sequence of membership queries (does the system accept a given timed word?) and equivalence queries (is a hypothesized description equivalent to the correct one?). In the constructed description, states are identified by sequences of symbols; timing constraints on transitions are learned by adapting algorithms for learning hypercubes. The number of membership queries is polynomially in the minimal zone graph and in the biggest constant of the automaton to learn for the first algorithm. The second algorithm learns a (usually) smaller representation of the underlying system.
Olga Grinchtein, Bengt Jonsson, Martin Leucker


Weitere Informationen