POK

Presentation

POK is an AADL partitioned runtime. It provides safety and security services to protect data and provide high availability. POK is written in C and uses C code generated by Ocarina (Ocarina has a dedicated code generator for POK). The code generator of POK configures the kernel to ensure space partitioning and enforce security policy described in the model.

POK runs on x86 and can be executed inside QEMU.

A poster was made to present the dedicated code generator for POK (called "Code Generation Strategies for Partitioned Systems" - you can see it in the papers section). A small presentation was written here.

Functionnalities

• Space partitioning (each partition own its own address space, POK enforces communication separation)
• Time partitioning (each partition is executed during a fixed timeslice)
• Integration of Lustre or Esterel application code
• Restrict functionnalities, only include required functionnalities
• Low complexity
• Low memory footprint

About

POK is written by Julien Delange and is written in the context of our work around AADL.

Official website

The official website of POK is available at http://pok.gunnm.org