POK configuration code can be automatically generated using AADL models. AADL models describe the overall architecture of a distributed system, including thread requirements, partitioning mechanisms and distribution specificities.
Before generate configuration/deployment or application code, a validation step can be issued on architecture models.
At first, in AADL models, potential errors are described at each level of the system. In consequence, we can check that all errors are recovered using an appropriate handler.
In AADL models, we express security requirements for each partition.
In the architecture models, scheduling requirements are specified. In particular, for each partition, we specify allocated time frames, as well as scheduling order. Moreover, in each partition, we specify the scheduling requirements of each threads (period/sporadic, period, deadline, etc …).
Using this information, we can check scheduling of AADL models. The Cheddar project provide verification facilities to check scheduling requirements of AADL models. It provides the ability to check scheduling requirements before implementation.
At this time, Cheddar is not included in the POK toolchain.