Before presenting recipes for AADL modeling and verification with
various AADL tools, please have a look on this page
first which introduce
the analysis tools assumed in AACB.
Information about the AADL language itself can be found [http://www.aadl.info on the AADL website itself].
Recipes
You have now at least a little background about AADL?
If so, let start with simple recipes which explain how to design and analyze AADL models.
Any recipe has the same layout, composed of 4 parts:
- System to model and assumptions: is usually a short description in natural language of the issue
we want to cover, i.e. the problem to solve, model and actually to analyze.
- Typical solution: dicusses a solution AADL proposes, in term of components and properties.
Those are kinds of design patterns that can be applied elsewhere.
- Possible analysis: discusses the analysis you can apply on the recipe with the tools considered in AACB.
- Case study: usually provides examples as a set of exercices with one or several possible solutions.
Here is the list of the recipes currently described in AACB:
In this first set of examples, we want to model and verify a
system composed of tasks, such as threads (Java or POSIX) or Ada tasks. Those tasks run concurrently and
are independent, which means that they do not interact or at least, we do not want to model this
interaction. In this recipe, we assume that tasks are run on a single processing unit,
e.g. a unicore processor for example.
In this second set of examples, we extend recipe 1 by modeling
a first interaction means: tasks
may share data through shared memories.
We also discuss about Ravenscar, a set of contraints related to this kind of interaction which
make analysis easier.
In this recipe, we still assume that tasks are run on a single processing unit,
e.g. a unicore processor for example.
For this second recipe,
we want to investigate systems that are composed of tasks organized as a directed acyclic graph, or DAG.
Tasks are connected to exchange data.
Again, recipe 3 assumes that tasks are run on a single processing unit, e.g. a unicore processor.
The previous recipes assumed a uniprocessor architecture.
In this set of recipes, we show how to model several categories of multiprocessor
systems such as multicore architectures, from the most predictable one upto the lest
predictable as migration
We first start
with recipe 4.1 describing an architecture where computing units (i.e. cores) have no
shared hardware resources (i.e. cache or memory units) and tasks are statically
allocated on the cores. Tasks cannot migrate from one core to another.
Tasks assigned on different
computing units cannot share software resources as there is not shared memory.
This kind of architecture is called a partitioned multiprocessor.
In recipe 4.2, we extend recipe 4.1 with shared software components. Recipe 4.2 shows
how to specify an architecture when several cores share a main memory. This kind
of architecture is sometimes referenced by the concept of core affinity.
It is also partitionned as tasks are always not allowed
to migrate from one core to another.
Finally, recipe 4.3 shows how to model global multiprocessors architectures.
With global multiprocessors, tasks may migrate at runtime and they share the same main memory.
While this last approach is supposed to provide the better performance, it leads also to the
less predictable timing behavior.
In the previous solutions, except the main memory, we globally ignore shared hardware resource,
Unfortunatelly, shared hardware resources lead to new kind of interference on the tasks.
Indeed, the tasks running on the core compete for the access to such hardware resources.
The 3 first recipes do not model shared hardware components because
interference due to such shared component are assumed to be negligeable in recipes 4.1 to 4.3.
In practice, for some systems, shared hardware resources interference cannot be
ignored and it is the topics of recipes 4.4. In this last
set of recipes, shared hardware
resource can be cache units of various types (data, instruction, L1 or L2),
other memory units and interconnection technologies
between computing and memory units. Recipes 4.4.1, 4.4.2 and 4.4.3
address these 3 aspects.
ARINC653 is a standard for avionic systems with timing and space isolation, which
is enforced with a two levels of hierarchical scheduling. Let see how to express this with AADL
and also to investigate schedulability.
In this recipe, we show how to model systems that are state machine
oriented and what kind of verification we can do on such model. AADL provides
the Behavioral annex for such purpose and the recipes in this section will rely on this annex.
State machines can be used for various rational and ojectives, as shown in the recipe list above:
In this recipe, we show how to model two applications run on different processors and
connected by a network.
Various models and analysis can be run in this recipe:
Redondancy is a classical mean
to increase safty in critical systems. This recipe shows how to model this
pattern and presents several variants such as active or passive redondancy.
MILS proposes an architecture which allows designers to
verify and enforce confidentiality and integrety contraints. In this recipe, we shows the required
properties to model such kind of architecture and also how to perform verifications such as
Bell and Lapadula.
An architecture model is usually a design solution of a system
that has a set of requirements to meet.
In this recipe, we explain how to
express requirements and their relationships to enforce tracability
with an AADL architecture.
We show how to do it with ALISA, allowing the verification that a AADL model is
compliant with a set of requirements.