Abstracts

A type-based analysis of causality loops in hybrid systems modelers

(Inria)
,
(Inria and DI, École normale supérieure)
,
(Inria)
,
(Esterel-Technologies)
, and
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)

Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete- and continuous-time behaviors with complex interactions between them. An important step in their compilation is the static detection of algebraic or causality loops. Such loops can cause simulations to deadlock and prevent the generation of statically scheduled code.

This paper addresses this issue for a hybrid modeling language that combines synchronous data-flow equations with Ordinary Differential Equations (ODEs). We introduce the operator last(x) for the left-limit of a signal x. The last(x) operator is used to break causality loops and permits a uniform treatment of discrete and continuous state variables. The semantics of the language relies on non-standard analysis, defining an execution as a sequence of infinitesimally small steps. A signal is deemed causally correct when it can be computed sequentially and only changes infinitesimally outside of announced discrete events like zero-crossings. The causality analysis takes the form of a type system that expresses dependencies between signals. In well-typed programs, signals are provably continuous during integration provided that imported external functions are also continuous.

The effectiveness of the system is illustrated with several examples written in Zélus, a Lustre-like synchronous language extended with ODEs.

Keywords: Hybrid systems; Synchronous programming languages; Type systems
Publisher: Elsevier
  • This is the journal version of a conference paper at HSCC 2014. It contains extra material and numerous small improvements.
  • This paper is accepted for Nonlinear Analysis: Hybrid Systems. It is available online now and will appear in print in November 2017.
  • A preprint is also available.
  • Examples and proofs are available online.

A Synchronous Look at the Simulink Standard Library

(Inria and DI, École normale supérieure)
,
(ANSYS/Esterel-Technologies)
,
(ANSYS/Esterel-Technologies)
,
(ANSYS/Esterel-Technologies)
, and
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)

Hybrid systems modelers like Simulink come with a rich collection of discrete-time and continuous-time blocks. Most blocks are not defined in terms of more elementary ones—and some cannot be—but are instead written in imperative code and explained informally in a reference manual. This raises the question of defining a minimal set of orthogonal programming constructs such that most blocks can be programmed directly and thereby given a specification that is mathematically precise, and whose compiled version performs comparably to handwritten code.

In this paper, we show that a fairly large set of blocks from the Simulink standard library can be programmed in a precise, purely functional language using stream equations, hierarchical automata, Ordinary Differential Equations (ODEs), and deterministic synchronous parallel composition. Some blocks cannot be expressed as they mix discrete-time and continuous-time signals in unprincipled ways and so are statically forbidden by the type checker.

The experiment is conducted in Zélus, a synchronous language that conservatively extends Lustre with constructs for programming systems that mix discrete-time and continuous-time signals.

Keywords: Hybrid systems; Synchronous programming languages; Type systems
Publisher: ACM

Symbolic Simulation of Dataflow Synchronous Programs with Timers

(IBM Research)
,
(Inria and DI, École normale supérieure)
, and
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)

The synchronous language Lustre and its descendants have long been used to program and model discrete controllers. Recent work shows how to mix discrete and continuous elements in a Lustre-like language called Zélus. The resulting hybrid programs are simulated with a numerical solver. In this article, we focus on a subset of hybrid programs where continuous behaviors are expressed using timers to measure time elapsing, nondeterministic guards, and invariants, as in Timed Safety Automata. We propose a source-to-source compilation pass to generate discrete code that, coupled with standard operations on Difference-Bound Matrices, produces symbolic traces that each represent a set of concrete traces.

Keywords: Synchronous programming languages; Timed automata; Symbolic simulation
Publisher: IEEE

Real-Time Ticks for Synchronous Programming

(CAU Kiel)
,
(Inria and DI, École normale supérieure)
, and
(Inria)

We address the problem of synchronous programs that cannot be easily executed in a classical time-triggered nor event-triggered execution loop. We propose a novel approach, referred to as dynamic ticks, that reconciles the semantic timing abstraction of the synchronous approach with the desire to give the application fine-grained control over its real-time behavior. The main idea is to allow the application to dynamically specify its own wake-up times rather than ceding their control to the environment. As we illustrate in this paper, synchronous languages such as Esterel are already well equipped for this; no language extensions are needed. All that is required is a rather minor adjustment of the way the tick function is called.

Keywords: Synchronous programming; Real-time systems; Physical time; Esterel
Publisher: IEEE

A formally verified compiler for Lustre

(Inria and École normale supérieure)
,
(École normale supérieure and Inria)
,
(Univ. Pierre et Marie Curie, CNRS, and Inria)
,
(Inria)
,
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)
, and
(Yale and Collège de France)

The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.

We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.

Keywords: Synchronous Languages (Lustre); Verified Compilation; Interactive Theorem Proving (Coq)
Publisher: ACM

Vérification de la génération modulaire du code impératif pour Lustre

(Inria and École normale supérieure)
,
(Univ. Pierre et Marie Curie, CNRS, and Inria)
,
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)
, and
(Collège de France)

Les langages synchrones sont utilisés pour programmer des logiciels de contrôle-commande d'applications critiques. Le langage Scade, utilisé dans l'industrie pour ces applications, est fondé sur le langage Lustre introduit par Caspi et Halbwachs. On s'intéresse ici à la formalisation et la preuve, dans l'assistant de preuve Coq, d'une étape clef de la compilation: la traduction de programmes Lustre vers des programmes d'un langage impératif. Le défi est de passer d'une sémantique synchrone flot de données, où un programme manipule des flots, à une sémantique impérative, où un programme manipule la mémoire de façon séquentielle. Nous spécifions et vérifions un générateur de code simple qui gère les traits principaux de Lustre: l'échantillonnage, les nœuds et les délais. La preuve utilise un modèle sémantique intermédiaire qui mélange des traits flot de données et impératifs et permet de définir un invariant inductif essentiel. Nous exploitons la formalisation proposée pour vérifier une optimisation classique qui fusionne des structures conditionnelles dans le code impératif généré.

Keywords: Langages synchrones (Lustre); Assistants de preuve (Coq); Compilation vérifiée

Loosely Time-Triggered Architectures: Improvements and Comparisons

(DI, École normale supérieure and Inria)
,
(Inria)
, and
(Inria and École normale supérieure)

Loosely Time-Triggered Architectures (LTTAs) are a proposal for constructing distributed embedded control systems. They build on the quasi-periodic architecture, where computing units execute nearly periodically, by adding a thin layer of middleware that facilitates the implementation of synchronous applications.

In this paper, we show how the deployment of a synchronous application on a quasi-periodic architecture can be modeled using a synchronous formalism. Then we detail two protocols, Back-Pressure LTTA, reminiscent of elastic circuits, and Time-Based LTTA, based on waiting. Compared to previous work, we present controller models that can be compiled for execution, a simplified version of the Time-Based protocol and optimizations for systems using broadcast communication. We also compare the LTTA approach with architectures based on clock synchronization.

Keywords: Quasi-Periodic Architecture; Loosely Time-Triggered Architecture; Time-Based LTTA; Back-Pressure LTTA
Publisher: ACM

Soundness of the Quasi-Synchronous Abstraction

(DI, École normale supérieure and Inria)
,
(Inria and DI, École normale supérieure)
, and
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)

Many critical real-time embedded systems are implemented as a set of processes that execute periodically with bounded jitter and communicate with bounded transmission delay. The quasi-synchronous abstraction was introduced by P. Caspi for model-checking the safety properties of applications running on such systems. The simplicity of the abstraction is appealing: the only events are process activations; logical steps account for transmission delays; and no process may be activated more than twice between two successive activations of any other.

We formalize the relation between the real-time model and the quasi-synchronous abstraction by introducing the notion of a unitary discretization. Even though the abstraction has been applied several times in the literature, we show, surprisingly, that it is not sound for general systems of more than two processes. Our central result is to propose necessary and sufficient conditions on both communication topologies and timing parameters to recover soundness.

Keywords: Distributed Embedded Systems; Real-Time Models; Verification; Model Checking; Synchronous Languages
  • This paper was presented at the FMCAD 2016 conference in Mountain View, California, USA in October 2016.
  • The full proceedings are freely accessible online. Our article is also directly available.

Sundials/ML: interfacing with numerical solvers

(Inria and DI, École normale supérieure)
,
(AIST)
, and
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)

We describe a comprehensive OCaml interface to the Sundials suite of numerical solvers (version 2.6.2). Noteworthy features include the treatment of the central vector data structure and benchmarking results.

Keywords: Foreign Function Interfaces; OCaml; Numerical Solvers
  • This work was accepted at the ACM Workshop on ML, but it was presented the next day during OCAML 2016 (both workshops were colocated with ICFP) in Nara, Japan, in September.
  • A brief abstract appears in the informal proceedings of the workshop. A longer description is under preparation.
  • The Sundials/ML software is available under a BSD license.

Mechanizing a Process Algebra for Network Protocols

(Inria and DI, École normale supérieure)
,
(NICTA and CSE, UNSW)
, and
(NICTA and CSE, UNSW)

This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.

Keywords: Interactive Theorem Proving; Isabelle/HOL; Process Algebra; Compositional Invariant Proofs; Wireless Mesh Networks; Mobile Ad hoc Networks
Publisher: Springer

Loosely Time-Triggered Architectures: Improvements and Comparisons

(DI, École normale supérieure and Inria)
,
(Inria)
, and
(Inria and DI, École normale supérieure)

Loosely Time-Triggered Architectures (LTTAs) are a proposal for constructing distributed embedded control systems. They build on the quasi-periodic architecture, where computing units execute ‘almost periodically’, by adding a thin layer of middleware that facilitates the implementation of synchronous applications.

In this paper, we show how the deployment of a synchronous application on a quasi-periodic architecture can be modeled using a synchronous formalism. Then we detail two protocols, Back-Pressure LTTA, reminiscent of elastic circuits, and Time-Based LTTA, based on waiting. Compared to previous work, we present controller models that can be compiled for execution and a simplified version of the Time-Based protocol. We also compare the LTTA approach with architectures based on clock synchronization.

Keywords: Distributed controllers; synchronous programming.
Publisher: IEEE
  • This paper was presented at the EMSOFT conference in Amsterdam in October 2015. An enhanced version is included in an ESWEEK special issue of ACM TECS.
  • The paper is available on IEEE Xplore.
  • The author's version is also available.
  • The source code to all models is available on Guillaume's website. The models are written in Zélus.

A Synchronous-based Code Generator For Explicit Hybrid Systems Languages

(Inria and DI, École normale supérieure)
,
(ANSYS/Esterel-Technologies)
,
(ANSYS/Esterel-Technologies)
,
(ANSYS/Esterel-Technologies)
, and
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)

Modeling languages for hybrid systems are cornerstones of embedded systems development in which software interacts with a physical environment. Sequential code generation from such languages is important for simulation efficiency and for producing code for embedded targets. Despite being routinely used in industrial compilers, code generation is rarely, if ever, described in full detail, much less formalized. Yet formalization is an essential step in building trustable compilers for critical embedded software development.

This paper presents a novel approach for generating code from a hybrid systems modeling language. By building on top of an existing synchronous language and compiler, it reuses almost all the existing infrastructure with only a few modifications. Starting from an existing synchronous data-flow language conservatively extended with Ordinary Differential Equations (ODEs), this paper details the sequence of source-to-source transformations that ultimately yield sequential code. A generic intermediate language is introduced to represent transition functions. The versatility of this approach is exhibited by treating two classical simulation targets: code that complies with the FMI standard and code directly linked with an off-the-shelf numerical solver (Sundials CVODE).

The presented material has been implemented in the Zélus compiler and the industrial Scade Suite KCG code generator of Scade 6.

Keywords: Hybrid modelling; synchronous programming; compilation.
Publisher: Springer

A mechanized proof of loop freedom of the (untimed) AODV routing protocol

(Inria and DI, École normale supérieure)
,
(NICTA and CSE, UNSW)
, and
(NICTA and CSE, UNSW)

The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is ‘loop free’ if it never leads to routing decisions that forward packets in circles. This paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.

Keywords: AODV; protocol verification; Isabelle/HOL.
Publisher: Springer

Showing invariance compositionally for a process algebra for network protocols

(Inria and DI, École normale supérieure)
,
(NICTA and CSE, UNSW)
, and
(NICTA and CSE, UNSW)

This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.

Keywords: Isabelle/HOL; process algebra; reactive systems; invariance proofs; network protocols
Publisher: Springer

A Type-based Analysis of Causality Loops in Hybrid Systems Modelers

(Inria)
,
(Inria and DI, École normale supérieure)
,
(Inria)
,
(Esterel-Technologies)
, and
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)

Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete- and continuous-time behaviors with complex interactions between them. A key issue in their compilation is the static detection of algebraic or causality loops. Such loops can cause simulations to deadlock and prevent the generation of statically scheduled code.

This paper addresses this issue for a hybrid modeling language that combines synchronous data-flow equations with Ordinary Differential Equations (ODEs). We introduce the operator last(x) for the left-limit of a signal x. This operator is used to break causality loops and permits a uniform treatment of discrete and continuous state variables. The semantics relies on non-standard analysis, defining an execution as a sequence of infinitesimally small steps. A signal is deemed causally correct when it can be computed sequentially and only changes infinitesimally outside of announced discrete events like zero-crossings. The causality analysis takes the form of a type system that expresses dependences between signals. In well-typed programs, signals are provably continuous during integration provided that imported external functions are also continuous.

The effectiveness of this system is illustrated with several examples written in Zélus, a Lustre-like synchronous language extended with hierarchical automata and ODEs.

Keywords: Hybrid systems; Synchronous programming languages; Type systems; Block diagrams; Static analysis
Publisher: ACM

A slow afternoon chez PARKAS and a very fast fly (a fun talk).

(Inria; ENS)
and
(ENS; Inria)

We briefly present a problem posed to use by Rafel Cases and Jordi Cortadella during a lunch organised by Gérard Berry (it is a variation of a classic problem). We propose solutions in the Simulink tool and our language Zélus.

Imagine two cars. One starts at Barcelona and travels at 50 km/hr toward Girona—a distance of 100 km. The other starts at Girona and travels at 50 km/hr toward Barcelona. Between the two is a fly travelling at 80 km/hr, initially from Barcelona toward Girona, and changing direction instantaneously whenever it meets either car. There are two questions.

  1. How many zig-zags does the fly do during the two hours of travel?
  2. Where will the fly be when the two cars reach their destinations?

We first modelled this problem in Simulink. The number of zig-zags, to our great surprise and pleasure, was 42! [Adams 1979] (Using R2012a with the ODE45 solver and a relative tolerance of 1 ⨯ 10-3.)

We then modelled the problem in Zélus. This gave an answer of 48. (Using the Sundials CVODE solver and a custom implementation of the Illinois algorithm.)

Obviously neither answer is correct since the system is not well defined at the instant the cars pass each other. The important questions are whether we should, or even can, statically detect and reject such cases? or stop with an error at runtime?

Keywords: Synchronous languages; Zélus; Simulink; Hybrid Modelling; Zero-crossings; Simulation
Publisher: Unpublished

seL4: from General Purpose to a Proof of Information Flow Enforcement

(NICTA and UNSW)
,
(NICTA)
,
(NICTA)
,
(NICTA)
,
(NICTA)
,
(NICTA)
,
(NICTA)
,
(NICTA)
,
and (NICTA and UNSW)

In contrast to testing, mathematical reasoning and formal verification can show the absence of whole classes of security vulnerabilities. We present the, to our knowledge, first complete, formal, machine-checked verification of information flow security for the implementation of a general-purpose mi- crokernel; namely seL4. Unlike previous proofs of information flow security for operating system kernels, ours applies to the actual 9,600 lines of C code that implement seL4, and so rules out the possibility of invalidation by implementation errors in this code. We assume correctness of compiler, assembly code, hardware, and boot code. We prove everything else. This proof is strong evidence of seL4’s utility as a separation kernel, and describes precisely how the general purpose kernel should be configured to enforce isolation and mandatory information flow control. We describe the information flow security statement we proved (a variant of intransitive noninterference), including the assumptions on which it rests, as well as the modifications that had to be made to seL4 to ensure it was enforced. We discuss the practical limitations and implications of this result, including covert channels not covered by the formal proof.

Keywords: Correctness proofs; Information flow controls; Mechanical verification
Publisher: IEEE

Zélus: A Synchronous Language with ODEs

(NICTA and Inria)
and
(Univ. Pierre et Marie Curie and DI, École normale supérieure and Inria)

Zélus is a new programming language for modeling systems that mix discrete logical time and continuous time behaviors. From a user's perspective, its main originality is to extend an existing Lustre-like synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as data-flow equations and hierarchical automata can be composed arbitrarily with ODEs in the same source code.

A dedicated type system and causality analysis ensure that all discrete changes are aligned with zero-crossing events so that no side effects or discontinuities occur during integration. Programs are statically scheduled and translated into sequential code which, by construction, runs in bounded time and space. Compilation is effected by source-to-source translation into a small synchronous subset which is processed by a standard synchronous compiler architecture. The resulting code is paired with an off-the-shelf numeric solver.

We show that it is possible to build a modeler for explicit hybrid systems à la Simulink/Stateflow on top of an existing synchronous language, using it both as a semantic basis and as a target for code generation.

Keywords: Hybrid systems; Hybrid automata; Synchronous languages; Block diagrams; Type systems
Publisher: ACM

Analyzing an Embedded Sensor with Timed Automata in Uppaal

(Inria and École normale supérieure)
and
(University of NSW)

An infrared sensor is modeled and analyzed in Uppaal. The sensor typifies the sort of component that engineers regularly integrate into larger systems by writing interface hardware and software.

In all, three main models are developed. For the first, the timing diagram of the sensor is interpreted and modeled as a timed safety automaton. This model serves as a specification for the complete system. A second model that emphasizes the separate roles of driver and sensor is then developed. It is validated against the timing diagram model using an existing construction that permits the verification of timed trace inclusion, for certain models, by reachability analysis (i.e., model checking). A transmission correctness property is also stated by means of an auxiliary automaton and shown to be satisfied by the model.

A third model is created from an assembly language driver program, using a direct translation from the instruction set of a processor with simple timing behavior. This model is validated against the driver component of the second timing diagram model using the timed trace inclusion validation technique. The approach and its limitations offer insight into the nature and challenges of programming in real time.

Keywords: Timed automata; Uppaal; Timing diagrams; Timed trace inclusion
Publisher: ACM

Challenges and Experiences in Managing Large-Scale Proofs

(NICTA)
,
(NICTA, UNSW)
,
(NICTA, UNSW)
, and
(NICTA, UNSW)

Large-scale verification projects pose particular challenges. Issues include proof exploration, efficiency of the edit-check cycle, and proof refactoring for documentation and maintainability. We draw on insights from two large-scale verification projects, L4.verified and Verisoft, that both used the Isabelle/HOL prover. We identify the main challenges in large-scale proofs, propose possible solutions, and discuss the Levity tool, which we developed to automatically move lemmas to appropriate theories, as an example of the kind of tool required by such proofs.

Keywords: Large-scale proofs; Isabelle/HOL; Interactive theorem proving
Publisher: Springer

A Hybrid Synchronous Language with Hierarchical Automata: Static Typing and Translation to Synchronous Code

(Inria)
,
(Inria)
,
(Inria)
, and
(DI, École normale supérieure)

Hybrid modeling tools like Simulink have evolved from simulation platforms into development platforms on which testing, verification and code generation are also performed. It is critical to ensure that the results of simulation, compilation and verification are consistent. Synchronous languages have addressed these issues but only for discrete systems.

Reprising earlier work, we present a hybrid modeler built from a synchronous language and an off-the-shelf numerical solver. The main novelty is a language with hierarchical automata that can be arbitrarily mixed with data-flow and ordinary differential equations (ODEs). A type system statically ensures that discrete state changes are aligned with zero-crossing events and that the function passed to the numerical solver has no side-effects during integration. Well-typed programs are compiled by source-to-source translation into synchronous code which is then translated into sequential code using an existing synchronous language compiler.

Keywords: Real-time systems; hybrid systems; synchronous Languages; block diagrams; compilation; semantics; type systems
Publisher: ACM

Non-Standard Semantics of Hybrid Systems Modelers

(Inria)
,
(Inria)
,
(Inria)
, and
(École normale supérieure)

Hybrid system modelers have become a corner stone of complex embedded system development. Embedded systems include not only control components and software, but also physical devices. In this area, Simulink is a de facto standard design framework, and Modelica a new player. However, such tools raise several issues related to the lack of reproducibility of simulations (sensitivity to simulation parameters and to the choice of a simulation engine).

In this paper we propose using techniques from non-standard analysis to define a semantic domain for hybrid systems. Non-standard analysis is an extension of classical analysis in which infinitesimal (the ε and η in the celebrated generic sentence ∀ε ∃η ... of college maths) can be manipulated as first class citizens. This approach allows us to define both a denotational semantics, a constructive semantics, and a Kahn Process Network semantics for hybrid systems, thus establishing simulation engines on a sound but flexible mathematical foundation. These semantics offer a clear distinction between the concerns of the numerical analyst (solving differential equations) and those of the computer scientist (generating execution schemes).

We also discuss a number of practical and fundamental issues in hybrid system modelers that give rise to non reproducibility of results, nondeterminism, and undesirable side effects. Of particular importance are cascaded mode changes (also called zero-crossings in the context of hybrid systems modelers).

Keywords: Non-standard semantics; hybrid systems; Simulink; synchronous languages; block diagrams; zero-crossings
Publisher: Elsevier

Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language

(Inria)
,
(Inria)
,
(Inria)
, and
(Univ. Pierre et Marie Curie; LIENS, École normale supérieure)

Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.

Starting from a minimal, yet full-featured, Lustre-like synchronous language, this paper presents a conservative extension where data-flow equations can be mixed with ordinary differential equations (ODEs) with possible reset. A type system is proposed to statically distinguish discrete computations from continuous ones and to ensure that signals are used in their proper domains. We propose a semantics based on non-standard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zero-crossings, and also allows the correctness of the type system to be established.

The extended data-flow language is realized through a source-to-source transformation into a synchronous subset, which can then be compiled using existing tools into routines that are both efficient and bounded in their use of memory. These routines are orchestrated with a single off-the-shelf numerical solver using a simple but precise algorithm which treats causally-related cascades of zero-crossings. We have validated the viability of the approach through experiments with the Sundials library.

Keywords: Real-time systems; hybrid systems; synchronous Languages; block diagrams; compilation; semantics; type systems
Publisher: ACM

New Results on Timed Specifications

(Inria)
,
(Aalborg University)
,
(Aalborg University)
,
(Inria)
,
(Ecole Centrale de Nantes)
,
(Aalborg University)
, and
(IT University of Copenhagen)

Recently, we have proposed a new design theory for timed systems. This theory, building on Timed I/O Automata with game semantics, includes classical operators like satisfaction, consistency, logical composition and structural composition. This paper presents a new efficient algorithm for checking Büchi objectives of timed games. This new algorithm can be used to enforce liveness in an interface, or to guarantee that the interface can indeed be implemented. We illustrate the framework with an infrared sensor case study.
Keywords: Timed automata; timed refinement; modelling; specification
Publisher: Springer
  • Published in Lecture Notes in Computer Science 7137, Recent Trends in Algebraic Development Techniques, Revised Selected Papers of the 20th International Workshop on Algebraic Development Techniques (WADT10), Schloss Etelsen, Germany, July 2010.
  • The submitted version is available.
  • The model described in Section 4 is available for download.
  • My main contribution to this workshop paper involved the adaptation of the infrared sensor case study from my PhD thesis, to the theory and tool developed by my coauthors.
  • There was a rigorous review process for inclusion in the proceedings of this workshop.

Modelling and Programming Embedded Controllers with Timed Automata and Synchronous Languages

(NICTA; UNSW CSE)

Embedded controllers coordinate the behaviours of specialised hardware components to satisfy broader application requirements. They are difficult to model and to program. One of the greatest challenges is to express intricate timing behaviours—which arise from the physical characteristics of components—while not precluding efficient implementations on resource-constrained platforms. Aspects of this challenge are addressed by this thesis through four distinct applications of timed automata and the synchronous languages Argos and Esterel.

A novel framework for simulating controllers written in an imperative synchronous language is described. It includes a transformation of synchronous models into timed automata that accounts for timing properties which are important in constrained implementations but ignored by the usual assumption of synchrony. The transformation provides an interface between the discrete time of synchronous programs and a continuous model of time. This interface is extended to provide a way for simulating Argos programs within the widely-used Simulink software.

Timed automata are well-suited for semantic descriptions, like the aforementioned transformation, and for modelling abstract algorithms and protocols. This thesis also includes a different type of case study. The timing diagram of a small-scale embedded component is modelled in more detail than usual with the aim of studying timing properties in this type of system. Multiple models are constructed, including one of an assembly language controller. Their interrelations are verified in Uppaal using a construction for timed trace inclusion testing.

Existing constructions for testing timed trace inclusion do not directly address recent features of the Uppaal modelling language. Novel solutions for the problems presented by selection bindings, quantifiers, and channel arrays in Uppaal are presented in this thesis. The first known implementation of a tool for automatically generating a timed trace inclusion construction is described.

The timed automata case study demonstrates one way of implementing application timing behaviours while respecting implementation constraints. A more challenging, but less detailed, example is proposed to evaluate the adequacy of Esterel for such tasks. Since none of the standard techniques are completely adequate, a novel alternative for expressing delays in physical time is proposed. Programs in standard Esterel are recovered through syntactic transformations that account for platform constraints.

Keywords: Timed Automata; Synchronous Languages; Argos; Esterel; modelling; real-time; Simulink; Stateflow; timing diagrams
Publisher: UNSW

Delays in Esterel

(NICTA; UNSW CSE)
and
(UNSW CSE)

The timing details in many embedded applications are inseparable from other behavioural aspects. Time is also a resource; a physical constraint on system design that introduces limitations and costs. Design and implementation choices are often explored and decided simultaneously, complicating both tasks and encouraging platform specific programs where the meaning of a specification is mixed with the mechanisms of implementation.

The Esterel programming language is ideal for describing complex reactive behaviours. But, perhaps surprisingly, timing details cannot be expressed without making significant implementation choices at early stages of design. We illustrate this point with an example application where reactive behaviour and physical time are intertwined.

A simple solution is proposed: add a statement for expressing delays in physical time. While there are similar statements or library calls in many programming languages, the novelty of our proposal is that the delay statements are later replaced with standard Esterel statements when platform details become available. Delays are thus expressed directly in terms of physical time, but later implemented as a discrete controller using existing techniques. This approach is familiar in control system design where analytical models are constructed in continuous time and then later discretized to produce implementations.

We present some ideas for performing the translation and outline some of the remaining challenges and uncertainties.

Keywords: Synchronous languages; Esterel; real-time programming; embedded controllers; control software
Publisher: Unpublished
  • Presented at the Daghstuhl workshop Synchron 2009, and published in the proceedings, and also available here.
  • The Synchron 2009 workshop was not referreed.
  • This paper is an abridged version of a chapter from my thesis.
  • The slides are online.

Automatically transforming and relating Uppaal models of embedded systems

(NICTA; UNSW CSE)
and
(UNSW CSE)

Relations between models are important for effective automatic validation, for comparing implementations with specifications, and for increased understanding of embedded systems designs. Timed automata may be used to model a system at multiple levels of abstraction, and timed trace inclusion is one way to relate the models.

It is known that a deterministic and tau-free timed automaton can be transformed such that reachability analysis can decide timed trace inclusion with another timed automaton. Performing the transformation manually is tedious and error-prone. We have developed a tool that does it automatically for a large subset of Uppaal models.

Certain features of the Uppaal modeling language, namely selection bindings and channel arrays, complicate the transformation. We formalize these features and extend the validation technique to incorporate them. We find it impracticable to manipulate some forms of channel array subscripts, and some combinations of selection bindings and universal quantifiers; doing so either requires premature parameter instantiation or produces models that Uppaal rejects.

Keywords: Timed trace inclusion; Uppaal; model transformation.
Publisher: ACM

Reliable device drivers require well-defined protocols

(NICTA; UNSW CSE)
,
(NICTA; UNSW CSE)
, and
(NICTA; UNSW CSE)

Current operating systems lack well-defined protocols for interaction with device drivers. We argue that this hinders the development of reliable drivers and thereby undermines overall system stability. We present an approach to specify driver protocols using a formalism based on state machines. We show that it can simplify device programming, facilitate static analysis of drivers against protocol specifications, and enable detection of incorrect behaviours at runtime.

Keywords: Device drivers; modelling; systems engineering
Publisher: Usenix
  • Published in Proceedings of the 3rd workshop on Hot Topics in System Dependability, article 3, Edinburgh, June 2007.
  • This workshop presentation describes Ryzhyk's work. I co-developed the underlying model, which applies much from Argos, Statecharts, and ultimately the idea of constraint-oriented specification originating in CSP and LOTOS.

A Timing Model for Synchronous Language Implementations in Simulink

(UNSW CSE; NICTA)
and
(UNSW CSE; NICTA; UNSW Asia)

We describe a simple scheme for mapping synchronous language models, in the form of Boolean Mealy Machines, into timed automata. The mapping captures certain idealised implementation details that are ignored, or assumed away, by the synchronous paradigm. In this regard, the scheme may be compared with other approaches such as the AASAP semantics. However, our model addresses input latching and reaction triggering differently. Additionally, the focus is not on model-checking but rather on creating a semantic model for simulating synchronous controllers within Simulink.

The model considers both sample-driven and event-driven execution paradigms, and clarifies their similarities and differences. It provides a means of analysing the timing behaviour of small-scale embedded controllers. The integration of the timed automata models into Simulink is described and related work is discussed.

Keywords: Synchronous languages; Simulink; Timed automata
Publisher: ACM

Formal Models in Industry Standard Tools: An Argos Block within Simulink

(UNSW CSE; NICTA)
and
(UNSW CSE; NICTA)

Simulink is widely used within industry for simulation and model-driven development, and reactive behaviours are often modelled using an add-on called Stateflow. Argos is one of the synchronous languages that have been proposed for the specification, validation and implementation of reactive systems. It is a rigorously defined graphical notation which, although not as powerful as Stateflow, is much less complicated. This paper describes the implementation of an Argos block for Simulink.

Keywords: Reactive systems; synchronous languages; Simulink; Stateflow; Argos
Publisher: Springer
  • Available in F. E. Tay, editor, International Journal of Software Engineering and Knowledge Engineering: Selected Papers from the 2005 International Conference on Embedded and Hybrid Systems, volume 15(2), pages 389–395, Singapore, April 2005.
  • The slides are online.