Abstracts
A typebased analysis of causality loops in hybrid systems modelers
Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete and continuoustime 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
dataflow equations with Ordinary
Differential Equations (ODEs). We introduce the operator
last(x)
for the leftlimit 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 nonstandard 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 zerocrossings. The causality analysis
takes the form of a type system that expresses dependencies
between signals. In welltyped 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 Lustrelike synchronous language extended with ODEs.
 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
Hybrid systems modelers like Simulink come with a rich collection of discretetime and continuoustime 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 discretetime and continuoustime 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 discretetime and continuoustime signals.
 This article will be presented at the 17th annual ACM SIGPLAN conference on Embedded Software (EMSOFT 2017), in Seoul, South Korea in October.
Symbolic Simulation of Dataflow Synchronous Programs with Timers
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 Lustrelike 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 sourcetosource compilation pass to generate discrete code that, coupled with standard operations on DifferenceBound Matrices, produces symbolic traces that each represent a set of concrete traces.
 This article will be presented at the 12th annual forum on Specification and Design Languages (FDL 2017), in Verona, Italy in September.
RealTime Ticks for Synchronous Programming
We address the problem of synchronous programs that cannot be easily executed in a classical timetriggered nor eventtriggered 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 finegrained control over its realtime behavior. The main idea is to allow the application to dynamically specify its own wakeup 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.
 This article will be presented at the 12th annual forum on Specification and Design Languages (FDL 2017), in Verona, Italy in September.
A formally verified compiler for Lustre
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.

A formally verified compiler for LustreTimothy Bourke, Lélio Brun, PierreÉvariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg
PLDI 2017 Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017  This article was presented at the 38th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2017), in Barcelona, Spain in June 2017.
 The talk was recorded and the slides are available.
 The compiler was made available to reviewers and passed the artefact evaluation process, but is not yet available online. We want to tidy up a few things before making a proper release.
Vérification de la génération modulaire du code impératif pour Lustre
Les langages synchrones sont utilisés pour programmer des logiciels de contrôlecommande 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é.
 Cet article a été présenté aux Journées Francophones des Langages Applicatifs (JFLA 2017) à Gourette aux Pyrénées en janvier 2017.
 L'article est disponible sur HAL.
Loosely TimeTriggered Architectures: Improvements and Comparisons
Loosely TimeTriggered Architectures (LTTAs) are a proposal for constructing distributed embedded control systems. They build on the quasiperiodic 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 quasiperiodic architecture can be modeled using a synchronous formalism. Then we detail two protocols, BackPressure LTTA, reminiscent of elastic circuits, and TimeBased LTTA, based on waiting. Compared to previous work, we present controller models that can be compiled for execution, a simplified version of the TimeBased protocol and optimizations for systems using broadcast communication. We also compare the LTTA approach with architectures based on clock synchronization.

Loosely TimeTriggered Architectures: Improvements and ComparisonsGuillaume Baudart, Albert Benveniste, Timothy Bourke
ACM Transactions on Embedded Computing Systems (TECS), 2016  This article is the journal version of a paper presented at EMSOFT in 2015. Compared to the conference paper, we include an overview of Zélus, improvements and simplifications to some proofs, and a new section on optimizations under specific network assumptions.
 The source code to all models is available on Guillaume's website.
Soundness of the QuasiSynchronous Abstraction
Many critical realtime embedded systems are implemented as a set of processes that execute periodically with bounded jitter and communicate with bounded transmission delay. The quasisynchronous abstraction was introduced by P. Caspi for modelchecking 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 realtime model and the quasisynchronous 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.
 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
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.
 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
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.
 This paper is an extended version of the work presented at ITP2014. It includes a small running example, several new or reworked explanatory paragraphs, and new figures. Besides the presentation, only a few minor technical details have changed.
 This paper appears in Volume 56, Issue 3 of the Journal of Automated Reasoning. A preprint is available.
 The proof scripts are available from the Archive of Formal Proofs (and also as a pdf file).
Loosely TimeTriggered Architectures: Improvements and Comparisons
Loosely TimeTriggered Architectures (LTTAs) are a proposal for constructing distributed embedded control systems. They build on the quasiperiodic 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 quasiperiodic architecture can be modeled using a synchronous formalism. Then we detail two protocols, BackPressure LTTA, reminiscent of elastic circuits, and TimeBased LTTA, based on waiting. Compared to previous work, we present controller models that can be compiled for execution and a simplified version of the TimeBased protocol. We also compare the LTTA approach with architectures based on clock synchronization.
 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 Synchronousbased Code Generator For Explicit Hybrid Systems Languages
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 dataflow language conservatively extended with Ordinary Differential Equations (ODEs), this paper details the sequence of sourcetosource 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 offtheshelf 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.
 This paper was presented at the ETAPS Compiler Construction (CC) conference in London in April 2015.
 The prepress and final versions are available.
 The Zélus compiler binary is available online. As are the source code and generated code from the paper.
A mechanized proof of loop freedom of the (untimed) AODV routing protocol
The Ad hoc Ondemand 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 penandpaper 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 reestablish most proof obligations automatically and identify exactly the steps that are no longer valid.
 This paper was presented at ATVA in Sydney in November 2014.
 The prepress and final versions are available.
 The proof scripts are available from the Archive of Formal Proofs (and also as a pdf file).
 Further information is available on the pages of the NICTA Concurrency group.
Showing invariance compositionally for a process algebra for network protocols
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.
 This paper was presented at ITP in Vienna in July. The slides are available (the cake was baked by someone else).
 The prepress and final versions are available.
 The proof scripts are in the Archive of Formal Proofs (and also as a pdf file).
 Further information can be found on the pages of the NICTA Concurrency group.
A Typebased Analysis of Causality Loops in Hybrid Systems Modelers
Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete and continuoustime 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 dataflow equations with Ordinary Differential
Equations (ODEs). We introduce the operator last(x)
for
the leftlimit 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 nonstandard
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 zerocrossings. The causality analysis
takes the form of a type system that expresses dependences between
signals. In welltyped 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 Lustrelike synchronous language extended with hierarchical automata and ODEs.

A typebased analysis of causality loops in hybrid systems modelersAlbert Benveniste, Timothy Bourke, Benoit Caillaud, Bruno Pagano, Marc Pouzet
HSCC '14 Proceedings of the 17th international conference on Hybrid systems: computation and control, 2014  This paper was presented at HSCC conference in Berlin in April 2014.
 Examples and proofs are available online.
 A journal version is also available.
A slow afternoon chez PARKAS and a very fast fly (a fun talk).
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.
 How many zigzags does the fly do during the two hours of travel?
 Where will the fly be when the two cars reach their destinations?
We first modelled this problem in Simulink. The number of zigzags, 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?
 Presented as a short amusement at the Daghstuhl workshop Synchron 2013 and published in the proceedings (p.126).
 A slightly longer abstract, the slides, the Zélus source, and the Simulink model are available.
 The Synchron 2013 workshop was not referreed.
seL4: from General Purpose to a Proof of Information Flow Enforcement
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, machinechecked verification of information flow security for the implementation of a generalpurpose 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.
 This paper was presented by Toby in May at the IEEE Symposium on Security and Privacy, San Francisco, CA, USA.
 Versions are available through IEEE Xplore and NICTA.
Zélus: A Synchronous Language with ODEs
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 Lustrelike synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as dataflow 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 zerocrossing 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 sourcetosource translation into a small synchronous subset which is processed by a standard synchronous compiler architecture. The resulting code is paired with an offtheshelf 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.

Zélus: a synchronous language with ODEsTimothy Bourke, Marc Pouzet
HSCC '13 Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013  This paper was presented at HSCC in Philadelphia in April. The slides are available.
Analyzing an Embedded Sensor with Timed Automata in Uppaal
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.
Challenges and Experiences in Managing LargeScale Proofs
Largescale verification projects pose particular challenges. Issues include proof exploration, efficiency of the editcheck cycle, and proof refactoring for documentation and maintainability. We draw on insights from two largescale verification projects, L4.verified and Verisoft, that both used the Isabelle/HOL prover. We identify the main challenges in largescale 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.
 This paper was presented at CICM (MKM track) in July 2012, where it won the best paper award.
 Published in Intelligent Computer Mathematics, LNCS 7362, pp 3248.
 The submitted version is available.
A Hybrid Synchronous Language with Hierarchical Automata: Static Typing and Translation to Synchronous Code
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 offtheshelf numerical solver. The main novelty is a language with hierarchical automata that can be arbitrarily mixed with dataflow and ordinary differential equations (ODEs). A type system statically ensures that discrete state changes are aligned with zerocrossing events and that the function passed to the numerical solver has no sideeffects during integration. Welltyped programs are compiled by sourcetosource translation into synchronous code which is then translated into sequential code using an existing synchronous language compiler.

A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous codeAlbert Benveniste, Timothy Bourke, Benoît Caillaud, Marc Pouzet
EMSOFT '11 Proceedings of the ninth ACM international conference on Embedded software, 2011  This paper was presented at EMSOFT in Taipei in October. The slides are available.
NonStandard Semantics of Hybrid Systems Modelers
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 nonstandard analysis to define a semantic domain for hybrid systems. Nonstandard 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 zerocrossings in the context of hybrid systems modelers).
 This paper appears in the Journal of Computer and System Sciences, Volume 78, Issue 3, pages 877–910.
 The preprint is also available.
Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language
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 fullfeatured, Lustrelike synchronous language, this paper presents a conservative extension where dataflow 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 nonstandard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zerocrossings, and also allows the correctness of the type system to be established.
The extended dataflow language is realized through a sourcetosource 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 offtheshelf numerical solver using a simple but precise algorithm which treats causallyrelated cascades of zerocrossings. We have validated the viability of the approach through experiments with the Sundials library.

Divide and recycle: types and compilation for a hybrid synchronous languageAlbert Benveniste, Timothy Bourke, Benoît Caillaud, Marc Pouzet
LCTES '11 Proceedings of the 2011 SIGPLAN/SIGBED conference on Languages, compilers and tools for embedded systems, pages 61–70, Chicago, USA, April 2011.  This paper was presented at LCTES in Chicago in April. The slides are available (and also without overlays).
New Results on Timed Specifications
 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
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 resourceconstrained 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 widelyused Simulink software.
Timed automata are wellsuited 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 smallscale 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.
 The thesis.
 At the UNSW library.
Delays in Esterel
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.
 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
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 taufree 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 errorprone. 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.

Automatically transforming and relating Uppaal models of embedded systemsTimothy Bourke, Arcot Sowmya
EMSOFT '08 Proceedings of the 8th ACM international conference on Embedded software, pages 59–68, Atlanta USA, October 2008.  This paper contains important improvements to an earlier technical report: UNSWCSETR0723.
 Most of the techniques described in the paper are implemented in a tool called urpal.
 The slides are online.
Reliable device drivers require welldefined protocols
Current operating systems lack welldefined 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.
 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 codeveloped the underlying model, which applies much from Argos, Statecharts, and ultimately the idea of constraintoriented specification originating in CSP and LOTOS.
A Timing Model for Synchronous Language Implementations in Simulink
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 modelchecking but rather on creating a semantic model for simulating synchronous controllers within Simulink.
The model considers both sampledriven and eventdriven execution paradigms, and clarifies their similarities and differences. It provides a means of analysing the timing behaviour of smallscale embedded controllers. The integration of the timed automata models into Simulink is described and related work is discussed.

A timing model for synchronous language implementations in simulinkTimothy Bourke, Arcot Sowmya
EMSOFT '06 Proceedings of the 6th ACM & IEEE International conference on Embedded software, pages 93–101, Seoul, October 2006.  The slides are online.
 This version includes a correction to the last sentence on page 7.
Formal Models in Industry Standard Tools: An Argos Block within Simulink
Simulink is widely used within industry for simulation and modeldriven development, and reactive behaviours are often modelled using an addon 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.
 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.