wiki:ArincAnnex
close Warning: Can't synchronize with repository "(default)" (Couldn't open Subversion repository /var/repositories/svn/aadl: SubversionException: ("Failed to load module for FS type 'fsfs'", 160033)). Look in the Trac log for more information.

ARINC653 Annex

TELECOM ParisTech is involved in the writing of the ARINC653 Annex for the AADL. This annex explain the modeling of ARINC653 architectures with the AADL. This page describe some modeling guidelines but also detail available tools that support this annex.

Modeling guidelines

Modeling partitions management

In ARINC653, partitions are managed using a dedicated module that enforce time and space partitioning across partitions. This kernel is also responsible to enforce isolation across inter-partitions ports (sampling and queuing ports). To model the kernel, we use the AADL processor component. We also add some properties to model time slices and their allocation to partitions.

Modeling partitions

We model partitions with the process and virtual processor components. The virtual processor models the scheduler and the internal runtime of each partition whereas the process component models the address space of the partition.

The process can be bound to memory components, to represent the different segment allocation on partitions. To do so, we add memory subcomponents in the main memory component to model memory segments inside the main memory component.

Modeling inter-partitions communications

Partitions can communicate using sampling and queuing ports. The queuing ports are mapped to AADL event data ports while sampling ports are mapped using AADL data ports. These features are added to the AADL process component that models the partition.

Modeling intra-partitions communications

ARINC653 Processes (AADL threads) can communicate using intra-partition communication services. Blackboard are modeled using AADL data ports while buffers are mapped to AADL event data ports.

Modeling security levels

To represent security constraints, we model security levels of each partition. We model the security layers with the AADL virtual bus component. Then, we add a property (POK::Security_Level) to detail the security level of this security layer.

This modeling approach has many advantages :

  • A bus can indicate which security layers are supported. In this case, the bus component contains the different security layers as virtual bus subcomponents.
  • A partition can indicate which security layers it supports by providing different virtual bus classes. This is done with the Provided_Virtual_Bus_Class property.

ARINC653 deployment file generation

Ocarina can automatically generate ARINC653 XML deployment-files from AADL models. To do that, simply use the POK generator with the ARINC653 flavor. You should invoke Ocarina like this:

ocarina -k arinc653 -k no-assert -aadlv2 -g pok <list of your aadl models>

An example of generated deployment file is given on our examples page

POK code generator and POK runtime

The POK code generator outputs C code for the POK runtime, which provides space and time isolation. The code from this generator uses a dedicated API that is only useful for our partitioned runtime, POK. However, we provide an option in the code generator to output ARINC653-compliant code. Thus, you can automatically generate C code that is compliant with the ARINC653 standard. To do so, invoke Ocarina like this:

ocarina -k arinc653 -k no-assert -aadlv2 -g pok <list of your aadl models>

The generated code should be written in a directory called generated-code. An example of generated code is given on our examples page

Last modified 5 years ago Last modified on 04/19/13 13:06:48