Institut National des Sciences Appliquéees Inrialpes
Aoraï plug-in (Aka LTL to ACSL)
Overview

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.

Installation

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).

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-help
Gives the whole list of options
Ressources (Last update: 25-02-2011 - 15:40:44)
Known Restrictions

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.

Contact

For any questions, remarks or suggestions, please contact   (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.

Valid HTML 4.01!   Any browser!   Valid CSS!