POK tries to be compliant with many standards of real-time embedded systems. At this time, we support the following standards:

• ARINC653, an avionics standard for safety-critical systems. POK supports time and space partitioning to isolate different partitions.
• MILS, an approach to build real-time embedded systems. Our MILS implementation relies on strong isolation of devices and partitioning services.

• Partitions support (time and space partitioning)
  • Intra-partition communication services
  • Inter-partitions communication services
  • Health-moniroting services (faults are contained in their partitions)
  • Hierarchical scheduler (fixed timeline for partitions, RMS/RR/EDF inside partitions)
• Available APIs
  • ARINC653 (Ada and C)
  • POK canonical API support
  • POSIX (partial implementation)
• Language support
  • C
  • Ada
• Real-Time scheduler (RMS/EDF/RR)
• Configuration through models (AADL)

• x86 with QEMU support
• PowerPC/prep

• x86/Linux
• x86/Mac OS X
• x86/Windows

The configuration of the system can be automatically generated using modeling languages. Configure a kernel is sometimes tedious, error-prone and an error could create errors and implies serious issues. In our approach, we use the AADL language to model the whole architecture of the system (partitions, threads, communications and so on). AADL is an architectural language that describes systems with their requirements and properties (partitions, threads, scheduling/ceiling protocoles). Using models, we can automatically application and kernel code.

A code generator for POK is available in the Ocarina AADL compiler. To get more information about AADL, please visit the official website of the language. You can also look at the aadl portal at TELECOM ParisTech

We provide some videos to demonstrate the use of POK with Eclipse and the AADL. You can check the following video out :

• ARINC653 example with two partitions with one thread in each partition
• ARINC653 example with two partitions with one thread and a communication channel between these partitions

In the video, we achieve the whole development process:

1. System modeling with Topcased
2. System verification using Ocarina/REAL
3. Automatic code generation using Ocarina
4. Compilation of generated code against POK
5. Execution in an Emulator (QEMU)