Model Based Software Engineering with AADL

Model Based Software Engineering with AADL

Full day tutorial, Sea UE teaching week, October 2022, Brest, France.

Frank Singhoff, Lab-STICC UMR CNRS 6285, Computer Science department, University of Brest

Exercise 1, basic analysis demo with AADLInspector

Exercise 2, first handouts with AADLInspector

Exercise 3, Mars PathFinder, analysis of a model with shared data

Exercise 4, code generation and design space exploration with Ocarina

Exercise 5, data port communications

SOLUTIONS

Exercise 1, basic analysis demo with AADLInspector

This set of exercises show how to use AADLInspector to run scheduling analysis with Cheddar.
The slides of the lecture to do those exercises can be downloaded here .

To do the following exercises, you need AADLInspector. You can download and install AADLInspector on your laptop (for Windows targets only). Just unzip the file to install the software on your laptop.

Move to the AI-1.8/bin folder and just click on the AADLInspector.exe file. The objective of this first exercise is to discover the basic analysis options of the tool.

Download the following AADL model. and save those files in a specific folder. Those files are composing an AADLInspector project: the file .aic allows AADLInspector to load all AADL files composing your model from the menu File/Load.
From File/Load, load the project.
With the Static analysis/Parse and Instanciante LMP button, verify the AADL model. What is the root component of this model? What is the instance model graph. Notice that the Static analysis/Parse Ocarina button makes more restrictive verifications with Ocarina in order to generate code for example.
To perform a scheduling analysis, the processor component has to be extended with few properties. Add to the cpu_leon2 component the following properties:
```
PROPERTIES
   Scheduling_protocol => (posix_1003_highest_priority_first_protocol);
```
Compute the scheduling of this thread set with Cheddar by the button Timing Analysis/Simulation timelines (Cheddar). From this simulation, compute with Cheddar the response times of the threads by the button Timing Analysis/Simulation Tests (Cheddar).
We can also compute theoretical worst case thread response times, always with Cheddar but with the button Timing Analysis/Theoretical Tests (Cheddar). Notice that theoretical worst case thread response times may differ from response times computed from simulation.

Exercise 2, first handouts with AADLInspector

In this exercise, we will model and analyze a set of threads writing or reading data from a shared memory area. We will assume that the shared memory area is modeled by a data component. Writing or reading an element will be modeled by the access of the data component in mutual exclusion. The objective of this exercise is to gradually build and analyze your first AADL models. With the 2 first questions, we will define independant threads, i.e. we do not model the shared memory area. In the last question, we extend the model with the thread communications.

Question 1 :

Download these AADL files .
Change the definition of the threads and the process above in order to:
- Define a periodic thread called writer with a deadline and a period of 10 ms. The priority is 20. The execution time of this thread is about 1 ms in the best case and 3 ms in the worst case.
- Define a periodic thread called reader with a deadline and a period of 20 ms. The execution time of this thread is about 2 ms. The priority is 10.
Check correctness of the model with the LMP static analysis. Remind that Ocarina can also be used for static analysis. Remind also that as Ocarina is used to generate code, the static analysis with Ocarina is more strict than LMP.
Do scheduling analysis with AADLInspector.

Question 2 :

From the model of the previous question and without introducing new component type, extend the model in order to declare 3 writers and 2 readers with the following properties:
- Writer 1 : Deadline = Period = 40 ms ; execution time ranging 1 and 5 ms ; Priority = 1
- Writer 2 : Deadline = Period = 20 ms ; execution time ranging 1 and 4 ms ; Priority = 2
- Writer 3 : Deadline = Period = 20 ms ; execution time ranging 1 and 2 ms ; Priority = 3
- Reader 1 : Deadline = Period = 40 ms ; execution time ranging 1 and 3 ms ; Priority = 4
- Reader 2 : Deadline = Period = 40 ms ; execution time ranging 1 and 2 ms ; Priority = 5
Verify your model by simulations with AADLInspector.

Question 3 :

We now extend the previous model with a data component to model thread communications.

Change your previous model by adding a data component and the required connections to the threads. For this question, we assume that only writer threads access to the shared data during their execution. For this data component, define the following property to forbid priority inversion:
```
properties
   Concurrency_Control_Protocol => PCP;
```
Once updated, analyze your model with AADLInspector to locate locks and unlocks of the data component.

Exercise 3, Mars PathFinder, analysis of a model with shared data

This exercise is a simplified architecture model of the Mars Pathfinder mission (see https://mars.nasa.gov/mars-exploration/missions/pathfinder/ for further details). In this exercise, you must look for a design mistake and propose a solution for it. In 1997, Mars Pathfinder casts a mobile robot called Sojourner on Mars. This mobile robot was controled by a multitask software running on a VxWorks target. This software was composed of the following tasks:

Tasks	Priorities	Periods/Deadlines	Executime time
SCHED_BUS	1	125 ms	25 ms
DATA	2	125 ms	25 ms
CONTROL	3	250 ms	25 ms
RADIO	4	250 ms	25 ms
VIDEO	5	250 ms	25 ms
MESURE	6	5000 ms	50 ms
FORECAST	7	5000 ms	Between 50 ms and 75 ms

All the tasks are periodic, synchronous, and have deadlines equal to periods.
FORECAST is sometimes released for a job of 50 ms, and sometimes for a job of 75 ms, depending of the size of the payload to handle.
Priority levels are VxWorks priorities: the lower the value is, the higher the priority level is.
DATA, CONTROL, MESURE and FORECAST required a shared data which is accessed by a critical section during all their execution times (i.e all their capacity/WCET). To reduce costs, those critical sections were implemented with a mutex that did not use inheritance priority protocol such as PIP or PCP. In order to define those critical sections without PIP/PCP, simply do not add the Concurrency_Control_Protocol property when defining your data component.

During the mission of Mars PathFinder, operators noticed that some deadlines were missed, leading to reboots of the system.
Download these AADL files and update this model to discover what are the missed deadlines and why those threads were not able to meet their deadlines.
How to solve this issue? Apply it on your AADL model.

Exercise 4, code generation and design space exploration with Ocarina

We want to model and verify the scheduling of an embedded software inside a fridge. This software controls the production of cold, an alarm associated with the door, the temperature as well as the lighting of the equipment.

You are asked to study the behavior of this system. It is assumed that the latter is composed of the following periodic tasks:

Threads	Execution time	Periods/deadlines
Thermostat	Never more than 2 ms	15 ms
Door	1 ms sometimes, 2 ms otherwise	30 ms
Lamp	Never more than 1 ms	7 ms
Alarm	Most of the time 2 ms, 3 ms in exceptional cases	10 ms
Probe	Never more than 2 ms	14 ms

Deadlines are equal to periods. The dates of first activation of all tasks are the same and is zero. At first, it is assumed that the threads are independent. It is also assumed a processor with a pre-emptive fixed priority scheduler and a prioritization according to Rate Monotonic.

Question 1 :

Here is the AADL model for verification purpose. Download those files, load them in AADLInspector and check the scheduling.
We now see how source code can be generated for this model. Save the new files of this folder. This is an example of an AADL model composed of 2 independent periodic threads (tic and tac). This example shows you how ocarina generates code. To do this, it is necessary to proceed as follow:
- Setting up your working space with this command:
```
 source ocarina.bash
```
- Generate C code from the AADL model:
```
 ocarina -x scenario.aadl
```
  .
- The generated C code is stored in the folder root_impl. It can be compiled with:
```
make
```
  In this folder, you should find a Linux binary (file node_a) that can be run from a Unix shell.
Study the generated files activity.h, activity.c, deployment.h and main.c. Explain their contents.
Adapt the fridge model with the tic/tac example in order to generate C code for your model of the fridge. For this question , you need this C file implementing a fake C application code, to be integrated with the generated code.

Question 2 :

Alarm and Thermostat threads share a data in mutual exclusion during all their execution time. This data stores the temperature measured by Thermostat. Thus, Thermostat modifies this data while Alarm only read it.

Modify the fridge AADL model updated to handle the shared data.
We give you a new version of tic/tac AADL model, available here which shows you how to integrate a data component. The shared data is modeled by the Counter component.
Generate the code for this new tic/tac example with Ocarina, compile and test the generated program.
Explain the content of types.h and types.c
Explain the role of tic_sequence and tac_sequence components.
Change your fridge model to integrate the data shared between Alarm and Thermostat in order to generate the C code with Ocarina.
Test this new fridge model with Ocarina.

Question 3 :

We want to divide the tasks on two processes mapped on two processors:

The Alarm and Thermostat tasks and their shared data are deployed on the first processor.
The Probe, Door, and Lamp tasks are deployed on the second processor.
Modify your AADL model accordingly, then build/test the code Ocarina.
What are the main differences in the code generated between the two versions?

Exercise 5, data port communications

The objective of this new exercise is to discover the use of data ports and to do design space exploration.

Question 1 :

One of the classic means of communicating information between two threads consists of using data ports. The use of data ports allows a set of threads to exchange messages periodically while respecting various constraints of consistency on the data. In particular, the transmission and reception time of messages are fixed and known: messages are sent when the sending thread finishes its execution while the messages are received when the receiving thread starts to run.

Download this AADL model.
This model includes threads connected by data ports (see figure above). Identify in this model the threads that receive or emit data. What protocol is used here?
Simulate the scheduling of this model. Is this consistent with thread priorities? Why? Identify when messages between T2 and T3 are sent or received.
Now we assume that the Timing property is set to Delayed. Simulate scheduling again. Explain what are the changes in the scheduling and in the way messages are sent/received.

Question 2 :

The figure above shows the architecture of a software composed of a set of periodic threads with the following parameters:

Threads	Periods and deadlines	Execution time	Priority
T1	1000 ms	200 ms	10
T2	1000 ms	200 ms	20
T3	1000 ms	200 ms	30
T4	1000 ms	100 ms	40
T5	1000 ms	100 ms	10
T6	1000 ms	500 ms	20
T7	1000 ms	400 ms	30

Propose an AADL model composed of one AADL process with all the threads in the figure and the table above. Simulate its scheduling. What can you see?
To address the problem identified in the previous question, we want to distribute this application on two processors. On the first processor, we assign T1, T2, T3 and T4. On the second processor will be placed all other tasks. Simulate the scheduling of this new model. What is the new problem we have now? One possible solution is to use the property Dispatch_Offset. Experiment with this property by setting it for T5, T6, and T7 threads. How does Dispatch_Offset change the scheduling? Does it solve all scheduling and communication constraints?
Let try to distribute the tasks on more than 2 processors. How many processors do we need to both meet deadline and communication constraints?