averest

Model-based Design of Reactive Embedded Systems

About Averest

Averest is a framework for the model-based design of reactive systems that supports the modeling, specification, simulation, compilation, formal verification, and synthesis of hardware and software for reactive embedded systems. It contains compilers for synchronous languages, a simulator for the latter, support for formal verification with temporal and other logics, and various transformations for the hardware and software synthesis of reactive embedded systems which also covers pure hardware circuits and pure software systems. Averest is developed by the Embedded Systems Group at the RPTU in Kaiserslautern and is the result of a long-term and still ongoing research effort.

ES-Plakat-800

Overall Design Flow

There is not a unique design flow using Averest so that we finally decided to not offer a complete tool as a product, but rather a library of functions that can be combined in many ways for conducting research about model-based design of reactive systems. Nevertheless, a typical design flow consists of the following steps that are explained in a little more detail below:

  • modeling the system behavior by our synchronous language Quartz
  • compilation of the Quartz model to synchronous guarded actions (the intermediate system representation of Averest)
  • simulation, causality/clock analysis, and formal verification
  • possible partitioning into distributed weakly endochronous components
  • code synthesis as HW or SW components

      • design_flow

      The following text explains the above steps in terms of the namespaces of the Averest library. For more details, please consult the API reference documentation.

      The Synchronous Language Quartz

      Synchronous languages are well-suited for the design of reactive systems. Their common paradigm is the perfect synchrony which means that most of the statements are executed as micro steps in zero time. Consumption of time is explicitly programmed by partitioning the micro steps using pause statements into macro steps that all take the same amount of logical time. Thus, concurrent threads run in lockstep and automatically synchronize at the end of a macro step. The introduction of micro and macro steps is not only a convenient programming model, it is also the key to generate deterministic single-threaded code from multi-threaded synchronous programs. Thus, synchronous programs can be executed on ordinary microcontrollers without complex process managers. As another advantage, the translation of synchronous programs to circuits is straightforward since both share the same model of computation. Moreover, the formal semantics of synchronous languages makes them particularly attractive for reasoning about program semantics and correctness. Further information on Quartz can be found in the following sources (see also the example programs below):

      Compilation

      The compiler functions under Averest.Quartz.Compile are used to translate Quartz programs to synchronous guarded actions which are defined in Averest.Systems.Aif. Most parts of the translation of Quartz statements to guarded actions have been formally verified. In particular, the translation covers schizophrenic local declarations which is a nontrivial issue in the compilation of synchronous languages.

      We distinguish between AIF modules and AIF systems. AIF modules have a compile context that consists of input signals like abrt (for aborting the behavior), susp (for suspending the behavior), prmt (to distinguish between strong or weak abortion/suspension), and strt (for starting the behavior), and output signals like insd (whether control-flow is still active inside), inst (whether the execution is instantaneous, i.e., done in zero time), and term (whether there is a control-flow active inside, but leaving the module). With this compile context, AIF modules can be called within other modules that have to determine the input signals of the compile context, and have to use the outputs of the latter. AIF systems do not have such a compile context and are therefore somehow closed systems, but they still assume inputs from the environment. Apart from declarations of the input/output/local variables, they mainly consist of guarded actions for the control and data flow that determines the behavior of the AIF system. There may also be specifications for formal verification, and drivers (special Quartz statements that determine the inputs of the module) for simulation.

      The Averest Intermediate Format (AIF) defined in Averest.Systems.Aif is used in Averest as the intermediate representation of systems. The following transformations are mainly based on converting AIF systems and modules into special forms for the further formal verification or synthesis.

      Code Transformations

      Averest provides various transformations under Averest.Transform to transform the AIF systems into equivalent ones. Most importantly, there are the following transformations:

      • Aggregate data types like arrays and tuples can be translated to scalar data types by Averest.Transform.Scalarize.
      • Bounded range numbers and bitvectors can be reduced to booleans using Averest.Transform.Bitblast to finally obtain simple boolean models that can be used for model checking and for hardware circuit synthesis.
      • Specifications given in linear temporal logic (LTL) are translated to omega-automata and/or fixpoints in CTL and the µ-calculus where the membership to safety, liveness, and fairness classes of temporal logic are respected.

      Formal Verification

      The namespace Averest.Analyze provides functions for the analysis like formal verification. In particular, it provides its own implementation of BDDs (binary decision diagrams) and its own SAT solver as well as solvers for ILP problems based on the simplex algorithm and the Fourier-Motzkin elimination.

      HW/SW Synthesis

      Finally, the namespace Averest.CodeWriter offers functions for writing out the guarded actions in various output formats like sequential programs (C, MiniC, etc.), hardware description languages like Verilog and VHDL, and for model checkers like NuSMV.

Installation, API Reference and Examples

Installation

Averest has been implemented in F# under .NET core and can therefore be used under Windows, Linux, and macOS. Since version 3.0, Averest is provided as a NuGet under the following address: https://www.nuget.org/packages/Averest which makes its use very convenient: All you need is the latest dotnet SDK which you can download from https://dotnet.microsoft.com/en-us/download for your computer.

Once you have installed dotnet, you may open an F# interactive session and just have to type #r "nuget: Averest, 3.0.0";; to download Averest 3.0.0 in your session. After this, you can open the modules to use the functions provided by Averest (see the API reference documentation). If you want to use Averest for your own software project, all you need is to add the package reference in your project file.

We do no longer provide executable programs like complete compilers, simulators, and model checkers, and instead will soon offer on this page some simple F# programs that will show how the functions in Averest can be called for these tasks to put together different design flows for hardware and software design or formal verification. You can then easily use these programs as fsx scripts or if wanted, you may also compile them to your personal executable programs.

API Reference

The API reference documentation lists details about the functions contained in the Averest package.

Quartz Program Examples

MiniC Program Examples

Research Papers

To learn more about the foundations and algorithms behind the Averest tools, see the following pages:

Contact

Averest is the result of still ongoing research efforts of the chair on embedded systems at the department of computer science of the university of Kaiserslautern. As a contact person, you may contact any person of the group, in particular, the head which is:

Prof.Dr. Klaus Schneider
Embedded Systems Chair
Department of Computer Science
RPTU Kaiserslautern
P.O. Box 3049
67653 Kaiserslautern, Germany
web page