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

Aoraï is now available in the main Frama-C distribution. It used to be available from http://amazones.gforge.inria.fr/aorai/, but the version currently hosted there is obsolete and won't compile with newer versions of Frama-C. 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 the property to be verified: .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 safety 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

Contact

Aoraï has been originally written by Nicolas Stouls (  , CITI Labs, AMAZONES team). It is currently maintained by CEA LIST as part of the main Frama-C distribution. See our contact page for more information.

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.