Model validation

Our toolchain automatically validates models requirements before generate code. It was made to help system designer in the verification of its architecture.

Our validation process is based on Ocarina and the REAL language, which is a constraint language for the AADL. Its quite similar than OCL language (designed for UML), except that is specific to AADL and thus, makes easier the validation of AADL model. You can have additional information about Ocarina and REAL on http://www.aadl.telecom-paristech.fr. With REAL, the user defines one or several theorems that express what we want to check.

There is a list of the theorems used in the POK toolchain and what we verify:

1. MILS requirements enforcements: we check that each partition has one security level and connected partitions share the same security levels. For that, the underlying runtime and the connections should support appropriate security levels.
2. Bell-Lapadula and Biba security policies: for connected partitions, we check the Bell-Lapadula and Biba security policies (no read-up/write-down, ...). With that, we ensure that the architecture is compliant with strict security guidelines.
3. Memory requirements: we check that required size by a partition is less important than the size of its bounded memory component. In other words, we check that the memory segment can store the content of the partition. We also check that the requirements described on partitions are correct regarding their content (threads, subprograms size, ...).
4. Scheduling requirements (Major Time Frame): for each processor component, we check that the major time frame is equal to the sum of partitions slots. We also check that each partition has at least one time frame to execute their threads.
5. Architecture correctness: we check that models contain memory components with the appropriate properties. We also check that process components are bound to virtual processor components.