Aoraï plug-in (Aka LTL to ACSL)

The Aoraï plug-in provides a method to automatically annotate a C program according to an LTL formula F such that, if the annotations are verified, then we ensure that the program respects F.

The classical method to validate annotations is to use Wp or Jessie plug-ins and the Why tool.

Installation Dependencies

The plug-in source code is available on its official web page. In order to install or update this plug-in, you need to have the Frama-C framework.

If you want to use LTL syntax for properties, then you have to install the ltl2ba tool in your current path. This tool is distributed under the GPL licence and converts a LTL formula into a Büchi automaton. You can find this tool on the homepage of its author Paul Gastin (ENS Cachan).

Usage

The plug-in is activated with one of the following command lines:

frama-c file.c -aorai-ltl file.ltl

frama-c file.c -aorai-automata file.ya

These two commands differ only by the syntax used to express to property to verify: .ltl files are described in a ltl like syntax, while .ya are description of automata in a yacc-like syntax.

Options are:

-aorai-verbose: Gives some information during computation, such as used/produced files and heuristics applied
-aorai-show-op-spec: Displays, at the end of the process, the computed specification of each operation, in terms of Büchi states and transitions.
-aorai-dot: Generates a dot file of the Büchi automaton. Dot is a graph format used by the GraphViz tool.
-aorai-acceptance: if set, considers acceptation states (Only on finite traces). If not, only the safty is verified.
-aorai-output-c-file file: Outputs the annotated program in file (defaults is to derive a name from the one of the first input file)
-aorai-help: Gives the whole list of options

Ressources

Other ressources can be found at the official web page of Aoraï.

Known Restrictions

Only the safety part of properties is check. The liveness part is not truly considered. Currently, a liveness property is only a restriction to the terminating state of the program that have to be an acceptation state. Hence, if the program terminates, then the liveness property is verified.
Currently, function pointers are not supported.
In the init state from the automaton, conditions on C-array or C-structure are not statically evaluated (it's an optimization) but are supported.

Contact

For any questions, remarks or suggestions, please contact Nicolas Stouls (CITI Labs, AMAZONES team).

End Note: to the question "Why this name: Aoraï ?" my answer is: why not ? Aoraï is the name of the taller reachable mount in the Tahiti island and its reachability is not always obvious.