POK is a partitioned operating system. It provides separation functionnalities to isolate different software components. With this separation, different software components can be collocated on the same machine ensuring safety and security enforcement:
The concept of partitioned architectures is introduced in ARINC653 and MILS standards. POK tries to provide a generic partitioned concept that can fit with these standards.
AADL is a modeling language that describes system architectures. With AADL, you can represent your runtime architecture (processor, partition, communications, etc.) and their constraints (security level of a partition, scheduling policy of a processor, etc.). Such a representation can be processed to validate system architecture.
In POK, we use the AADL to generate the code of the kernel. You model your system with its partitioning constraints using AADL. Then, a code generator automatically generate the code that configures kernel and partitions. Using this development method, you avoid manual code production, which is, most of the time, error-prone.
Since Ocarina does not seems to be supported by TELECOM Paristech, the European Space Agency maintain its own version and continues to add new features and functionalities. You can get the sources of Ocarina at the following address: http://download.tuxfamily.org/taste/snapshots/sources/ocarina/
Installation instructions can be found on safety-critical.net.
Then, you will need to compile, build and install it (you will need an Ada compiler for that). Binaries releases are also available but does not seem to work on all systems because it requires some shared libraries related to GNAT (binaries on http://download.tuxfamily.org/taste/snapshots/binaries/ocarina/).
Yes, but in that case, you'll lose code generation benetifs and you'll have to write the configuration code of the kernel by yourself. The documentation of POK provides necessary items to configure POK by yourself.
At this time, POK supports ARINC653 and MILS standards. For ARINC653, the C layer is available. For MILS, we check MILS compliance at the model-level, with an AADL model validator.
POK is a free-software (free as in “free speech”, not as in “free beer”): the code is released under the BSD license. You can modify, adapt code and join our developer team.