--- layout: plugin title: Aoraï description: Verify specifications expressed as LTL (Linear Temporal Logic) formulas. key: verifying ---
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.
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.
Options are:
Other ressources can be found at the official web page of Aoraï.
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.