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.
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).
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.yaThese 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.
- Gives some information during computation, such as used/produced files and heuristics applied
- Displays, at the end of the process, the computed specification of each operation, in terms of Büchi states and transitions.
- Generates a dot file of the Büchi automaton. Dot is a graph format used by the GraphViz tool.
- 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)
- Gives the whole list of options
Other ressources can be found at the official web page of Aoraï.
- Only the safety part of properties is checked. 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.
Aoraï has been originally written by Nicolas Stouls ( 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.