This page gives some examples and case studies we made during our experiments with POK. These examples are available in POK releases, in the
examples directory. They illustrate the partitioning concept of POK and how we enforce safety and security during system execution.
The integrated example is an avionics architecture. This example is taken from the official AADL website and was designed to experiment the modeling of avionics architecture with the AADL. We took this example and adapt it to describe an ARINC653 architecture in order to run on top of POK. If the example from the AADL website provides only an architecture view, we also added the application code.
A complete description of this example is available on this page.
The ardupilot example is a mapping from the Arduino autopilot system. The original system was designed to run on SPARKfun platforms. We adapt the code, designed the underlying partitioned architecture to create a complete autopilot system that runs on top of POK.
Details and description of this example is available on this page.
The MILS example defines six partitions with different security levels that runs on several processors. Three SLS (Single Level of Security) partitions are running on a processor while three other SLS partitions are running on another processors. These partitions have different security levels (Top-Secret, Secret, Unclassified) and communicate data across the same bus.
This example emphasize how we can build MILS architectures with the AADL. It shows how we can use an encryption layers to secure data and enforce security even if shared devices don't provide security separation.
A more precise description of this example can be found on this page.