The Aoraï plug-in for Frama-C 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 the Jessie plug-in and the Why tool.
The plug-in source code is available in the resources section. In order to install 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 to property to verify: .ltl files are described in a ltl like syntax, while .ya are description of automata in a yacc-like syntax.
Currently, the switch statement is not supported and only the safety part of the LTL formula is check. The variant generation is a future for the implementation.
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.