4. Usage

4.1. Ocarina command-line

Ocarina has a rich command-line interface, covering all required steps to parse, instantiate, analyze or generate code from AADL models.

-h, --help

Display help and exit


Display version and exit

-v, --verbose

Output extra verbose information


Quiet mode (default)


Debug mode


Output default search directory, then exit


AADL version, ARG = 1 for AADL 1.0, 2 for AADL 2.x


Parse predefined non-standard property sets


Deactivate annex ARG

-r ARG

Use ARG as root system

-o ARG

Specify output file/directory


Automatically load AADL files


Add ARG to the directory search list


Parse and instantiate the model


Instantiate the model


Parse AADL file as an AADL scenario file

-g ARG

Generate code using Ocarina backend ‘ARG’


List available backends


Generate SPARK2014 annotations


Compile generated code


Clean code generated

-k ARG

Set POK flavor (arinc653/deos/pok/vxworks)


Run Ocarina in terminal interactive mode

-real_theorem ARG

Name of the main REAL theorem to evaluate

-real_lib ARG

Add external library of REAL theorems


Continue evaluation of REAL theorems after first failure (REAL backend)

-boundt_process ARG

Generate .tpo file for process ARG (Bound-T backend)


Compute coverage metrics


Execute system


Generate ASN1 deployment file (PolyORB-HI-C only)


Enable profiling with gprof (PolyORB-HI-C only)


A man page is also installed in Ocarina installation path, in $OCARINA_PATH/share/man/man1/.

4.2. ocarina-config

ocarina-config returns path and library information on Ocarina installation. This script can be used to compile user program that uses Ocarina’s API.

Usage: ocarina-config [OPTIONS]
        No option:
            Output all the flags (compiler and linker) required
            to compile your program.
            Output the directory in which Ocarina architecture-independent 
           files are installed, or set this directory to DIR.
            Output the directory in which Ocarina architecture-dependent 
           files are installed, or set this directory to DIR.
            Output the version of Ocarina.
            Output Ocarina's configuration parameters.
            Checks the validity and the presence of the given runtime and 
            then, outputs its path. Only one runtime can be requested at 
            a time. If no runtime name is given, outputs the root directory
            of all runtimes.
            Output the linker flags to use for Ocarina.
            Output the path to GNAT Project files for Ocarina
            Output the location of the standard property file.
            Output the location of resource files 
            (typically the standard properties)
            Output the compiler flags to use for Ocarina.
            Output this message