Averest is a framework for the specification, verification, and implementation of reactive systems. It can be used to build various tools targeting software in embedded systems, concurrent programs in general and hardware design.
It is developed by the Embedded Systems Group at the Technical University of Kaiserslautern. For more information, please see the documentation for technical details. Executables can be obtained on the download page. If you have any questions or comments regarding our tools or web pages, please contact us.
The Averest project aims at providing a complete set of tools for the development of reactive systems. Currently, it consists of the following components: a compiler for translating synchronous programs to our intermediate format, a set of transformations, a symbolic model checker, and a tool for hardware/software synthesis. Thus, Averest already covers large parts of the design flow of reactive systems from the specification to the implementation.
The design flow using Averest consists of the following steps: First, the system is described as a program in our imperative synchronous language Quartz. Then, the program is translated to synchronous guarded actions, which are the base of the Averest Intermediate Format (AIF) using the Quartz compiler qrz2aif. This intermediate description can be directly used for simulation with the simulator aif2trc. Furthermore, it can be used by the symbolic model checker SMV or the interactive theorem prover HOL to check whether the system satisfies its specifications. If this is the case, it can be synthesized using the various aif2* tools, which are able to generate an implementation in hardware or software.
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 operating systems. As another advantage, the translation of synchronous programs to circuits is straightforward. Moreover, the formal semantics of synchronous languages makes them particularly attractive for reasoning about program semantics and correctness.
Key features of Quartz are generic statements to describe parameterized systems, different forms of parallel execution (synchronous, asynchronous, interleaved), nondeterministic choice, event and state variables, integers of infinite and finite bitwidth as well as multi-dimensional array types.
The compiler qrz2aif is used to translate Quartz programs to synchronous guarded actions. Most parts of the translation of Quartz statements to transitions implemented in Ruby have been formally verified using the HOL theorem prover. In particular, the translation covers schizophrenic local declarations which is a nontrivial issue in the compilation of synchronous languages.
The Averest Intermediate Format
The Averest Intermediate Format (AIF) is a file format designed for describing synchronous systems at an intermediate level. Its main purpose is to serve as a language for exchanging system descriptions between the Averest component. AIF is based on the Extensible Markup Language (XML) and is not intended for interaction with human users, though it can be used for this purpose. The following features were essential for the design of AIF:
- general-purpose format that can be used for various applications
- flexibility and ease of use on the basis of a standardized language
- support for higher data types such as integers of arbitrary size
Since AIF is based on the Extensible Markup Language (XML), it is independent of operating systems and encodings. Additionally, most programming languages offer support for XML and there is large number of tools for processing XML files, e.g. parsers and converters. AIF follows the style of guarded actions, a well-established model for the description of concurrent systems. This simplifies the semantics and provides a high degree of flexibility.
Averest provides various transformations to prepare the synchronous guarded actions obtained by the compilation for synthesis. For example:
- Aggregate data types like arrays and bitvectors can be translated to scalar data types. This allows to translate Quartz programs to hardware circuits and also to interface Averest with many other tools that are not able to deal with such data types directly.
- Specifications given in linear temporal logic (LTL) even with an anchored version of past operators are translated to omega-automata and/or fixpoints in CTL and the µ-calculus. Averest currently offers two translations that respect the membership to safety, liveness, and fairness classes of temporal logic. Moreover, specifications may also be parameterized, e.g. to specify parametric conjunctions.
Built-in verification is provided by a symbolic model checker for finite and infinite state systems. As usual in symbolic model checking, finitesets are encoded by their characteristic functions in propositional logic using binary decision diagrams (BDDs). For the representation of infinitesets, however, more powerful logics are required, since propositional logic is naturally limited to the representation of finite sets. For that purpose, we use Presburger arithmetic, a decidable first-order predicate logic over the integers with addition as the basic operation. In the same way, we lift the specification language from propositional logic to Presburger arithmetic. As the specification language, Averest uses the µ-calculus which subsumes popular temporal logics such as CTL and LTL. Even though the µ-calculus is very powerful, it is commonly viewed as some sort of ‘assembly’ language for verification. For this reason, Averest includes a translator from FairCTL, an extension of CTL with fairness constraints, to the µ-calculus.
The synthesis tools aif2* translating system descriptions in AIF to hardware or software. Moreover, they can be used as a converter for third-party tools, e.g. other model checkers. Currently, the supported languages include ISO C, LEGO C, SystemC, Java, Standard ML, Verilog and VHDL.
For Verilog or VHDL output, finite state machines are generated that can be used as input for other tools such as FPGA compilers to build hardware. The C output can be used for simulation or for a direct implementation on a micro-controller. For that purpose, functions are provided to set the inputs and to get the outputs of a program.
- Version 2.2, 2011
Averest is implemented in F# which requires a .NET or mono framework for the execution of the generated executables. Windows 7, Windows Vista already contain the .NET framework, while an additional installation of .NET may be necessary for Windows XP, and an installation of mono might be necessary for Mac OSX and Linux versions.
For Windows XP, you may therefore have to first install .NET by downloading the automatic installer from Microsoft. We found out that .NET 4.0 is not sufficient when installed on Windows XP with Service Pack 2, but you need .NET 3.5 (and .NET 4.0 can be installed in parallel).
For Linux and Mac OSX, you have to download the “.NET equivalent” Mono. We are not aware of problems with the actual version.
For the compilation and simulation of Quartz files, everything else is contained in the Averest distribution. For the further use of the generated files like the C or Verilog files, you need further compilers which are not included in Averest.
If you are interested in using model checking, we currently only offer a translation to SMV, which is a popular model checker. The files generated by SMV should run under all versions of SMV. We recommend NuSMV which is an open source project that also offers compiled binaries for Windows and Linux. For Mac OSX, you have to compile NuSMV from the source files.
For illustrating dependencies of actions, some tools generate graphs that are written in files used by the GraphViz software. Again, this software is available for free for Windows, Linux and Mac OSX under the link listed below.
See the following links for more information on the additionally required tools:
User Manual and Technical Documentation
- Averest Mini-HowTo, Version 2.2, 2011.
- Quartz Language Reference Card , Version 2.2, 2013.
- Quartz Introduction Slides, 2012.
- The Synchronous Programming Language Quartz , Version 2.0, 2009.
To learn more about the foundations and algorithms behind the Averest tools, see the following pages:
Before you download Averest, we would apprecciate if you tell us your name and affiliation.
For any information, features, suggestion or comments please feel free to leave us a message. You can use the contact form below.