Architecture validation

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.

In the remainder of this page, we give validation we made on AADL models. These verification can be issued on AADL files and are implemented in the AADL-compiler or its plugin for OSATE.

Safety validation

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.

Security validation

In AADL models, we express security requirements for each partition.

Memory requirements validation

Scheduling validation

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.

architecturevalidation.txt · Last modified: 2012/05/10 16:11 by julien