|
|
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 transition systems, 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. Even though the tools are part of a common framework, they are largely independent of each other and can also be used together with third-party tools.
The design flow using Averest consists of the following steps: First, the system is described as a program in our synchronous language Quartz, a descendent of Esterel. Then, the program is translated to a transition system in the Averest Interchange Format (AIF) using the Quartz compiler Ruby. This intermediate description can be directly used for verification with the symbolic model checker Beryl to check whether the system satisfies its specifications. If this is the case, it can be synthesized using Topaz that is able to generate an implementation in hardware or software.
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 macrosteps 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.
Ruby is used to translate Quartz programs to symbolic representations of transition systems. Depending on the used types (integers with infinite or finite bitwidth), the transition systems will have infinitely or finitely many states. The translations done by Ruby take into account different aspects of Quartz programs:
Generic statements are expanded which allows the convenient implementation of parameterized systems that may have n threads, bitvectors with n bits, arrays with n elements, etc.
Aggregate data types like arrays and bitvectors are 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.
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.
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. Ruby 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.
Beryl is a symbolic model checker for the verification of finite and infinite state systems. As usual in symbolic model checking, finite sets are encoded by their characteristic functions in propositional logic using binary decision diagrams (BDDs). For the representation of infinite sets, 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. An important aspect concerning efficient implementations is that every Presburger formula can be translated to a finite automaton that encodes its models. As there exists for every finite automaton an equivalent minimal one, automata can serve as a canonical normal form for Presburger formulas. This is very much in the same spirit as BDDs are used as a canonical normal form for propositional logic. Thus, automata can be viewed as a generalization of BDDs for the representation of infinite sets.
Infinite state systems occur in many areas in can be roughly classified as follows:
The ability to deal with data types over infinite domains makes Beryl attractive for the verification of datapaths without considering implementation specific details such as the bitwidth. In particular, there is no need to break a design down to Boolean expressions, as it is required for BDD based symbolic model checkers. For instance, large parts of microprocessors and assembler programs can be easily modeled in Presburger arithmetic. This is also an important step towards the verification in early design phases where higher data types are used to model systems at an abstract level. Nevertheless, Beryl can also be used to efficiently reason about finite state systems and digital circuits at the level of propositional logic.
As the specification language, Beryl 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, Beryl includes a translator from FairCTL, an extension of CTL with fairness constraints, to the µ-calculus. To check µ-calculus formulas, Beryl contains algorithms for global, local, and a variant of bounded model checking that can be used independently of the chosen base logic. There are many differences between these algorithms, in particular, global and local model checking algorithms follow radically different paradigms: while global model checking algorithms use fixpoint iteration to check a specification, local model checking algorithms are based on the construction of proof trees (tableaux) using syntax directed decomposition rules. The idea of bounded model checking is to reduce the verification problem to a satisfiability problem of the base logic, so that sophisticated SAT solvers can be employed to check the resulting formula.
For finite state systems, it is beneficial to be able to choose between different algorithms, since their runtimes may vary significantly. For example, safety properties can often be proved most efficiently using local model checking that incorporates induction-like reasoning. In contrast, bounded model checking is often superior when disproving a safety property by efficiently searching for a counter-example. For infinite state systems, however, the choice of the best algorithm is not primarily a matter of efficiency, but rather a matter of termination. Note that transition systems defined in Presburger arithmetic are as powerful as Turing machines, and hence, most verification problems are undecidable for such systems. For instance, due to the different nature of global and local model checking algorithms, it may happen that one algorithm terminates for a given specification while the other does not, and vice versa. For this reason, Beryl contains different model checking algorithms and heuristics to achieve termination for a large class of specifications. Additionally, the implemented algorithms can even be combined. As an example, given a nested fixpoint formula, the outer fixpoint can be solved using local model checking and the inner one using global model checking. In this way, the class of specifications that can be checked automatically is extended even further.
Beryl can also be used to determine tight bounds on the worst case execution time (WCET) of Quartz programs and other transition systems at an architecture independent level. WCET analysis is a crucial concern in the design of embedded systems, e.g. safety critical applications often require that certain tasks are completed before a strict deadline. One of the main problems of WCET analysis is that the number of executed instructions may heavily depend on the input data, in particular, the number of loop iterations may vary significantly. Using symbolic state space exploration techniques, however, it is possible to obtain exact information on the number of executed instructions.
Beryl has a modular structure to support various data structures and decision procedures. Technically, the modules have uniform interfaces and are selected during compile time. At the level of integers, one can choose between ordinary n-bit numbers and integers of arbitrary size. At the level of propositional logic, there are modules for the BDD packages CUDD and BuDDy and an interface to the SAT solver zChaff. The zChaff module behaves very much like a BDD package, e.g. the translation from arbitrary Boolean functions to sets of clauses is hidden in the module. Similar to BDD packages, all functions are stored in a manager and (syntactically) equivalent subexpressions are shared using hash tables and reference counters. Additionally, there are look-up tables to avoid that satisfiability of a function is checked multiple times, and simple logic minimization procedures to reduce the size of the formulas.
At the level of Presburger arithmetic, there are currently two decision procedures based on deterministic and alternating finite automata. A major advantage of the latter is that they can be composed in constant time which often significantly speeds up the contruction of the transition relation. However, since quantification is a hard operation on alternating automata, they are restricted to bounded model checking. For both types of automata, a semi-symbolic encoding is used where the states are represented explicitly, and the transitions are represented implicitly by means of propositional logic. In this way, traditional algorithms from automata theory such as the subset construction for determinization can be applied without relinquishing the compact symbolic representation. For deterministic finite automata, several minimization algorithms have been implemented that are called dynamically like variable reordering algorithms in BDD packages. Moreover, there are two procedures for checking equivalence, one is based on depth-first search and the other on Tarjan's union-find algorithm.
Topaz is a tool for translating system descriptions in AIF to hardware or software. Moreover, it can be used as a converter for third-party tools, e.g. other model checkers. Currently, the following languages are supported:
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.
The Averest Interchange Format (AIF) is a file format designed for describing reactive systems at an intermediate level. Its main purpose is to serve as a language for exchanging system descriptions between the Averest tools. 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:
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 functional languages, i.e., there are no imperative statements but only expressions. This simplifies the semantics and provides a high degree of flexibility. For example, an AIF file can contain multiple transition systems, and the result of evaluating a formula can be used to construct new formulas. AIF can also be 'abused' as a pocket calculator, e.g. to check satisfiability of propositional formulas.