-------------------------
 AADL INSPECTOR EXAMPLES
-------------------------
The examples are organized in projects (files with a .aic extension):
Deploy the tree in the left hand side browser and select a project 
by clicking on the corresponding icon.
Elements can be individually selected or deselected by a simple click 
on its icon.

Only the files that have an icon with a green tick will be processed.
The available processing tools are in the right hand side tabs:
* static analysis: various predefined parsing and processing tools
* lamp lab: custom analysis tools with LAMP annexes
* timing analysis: schedulability analysis, simulation and flow latency
* safety & security analysis: Fault Tree Analysis and Security Rules checker
* code generation: interface to launch Ocarina back-ends
* doc generation: quickly build an analysis report in PDF

Summary of proposed examples:

A: denotes use of AADL ARINC 653 Annex
B: denotes use of AADL Behavior Annex
C: denotes use of AADL Core 2.2 (SAE AS-5506C)
E: denotes use of AADL Error Modelling Annex (EMV2)
L: denotes use of AADL LAMP Annex (model processing language)
S: denotes use of simulation scenario (.asc files)

- patterns.aic: 
Contains seven sub-projects listed below. 
They illustrate the main communication and scheduling protocols that 
are supported by AADL and can be analysed with AADL Inspector.

  - dataflow.aic: [BCS]
  Dataflow communication between threads. 
  It can be used to observe the effect of Sampled, Immediate and 
  Delayed data port connections.

  - messages.aic: [BC]
  Message based communication between threads using queued events. 
  It can be used to observe input queue overflow.

  - shared_data.aic: [BC]
  Shared data communication between threads with critical sections. 
  It can be used to observe the effect of the Priority_Ceiling_Protocol 
  to avoid a deadlock.

  - client_server.aic: [BC]
  Subprogram call communication between threads. 
  It can be used to observe the effect of the client-server 
  synchronisation protocols.

  - arinc653.aic: [AC]
  Two layer hierarchical scheduling. 
  It can be used to investigate time and space partitioned systems 
  with the AADL ARINC653 Annex.

  - scheduling.aic: [C]
  Illustration of the supported scheduling protocols: 
  Rate Monotonic (RM), 
  Deadline Monotonic (DM), 
  High Priority First (HPF), 
  Round Robin (RR) and 
  Earliest Deadline First (EDF).

  - dispatching.aic: [CS]
  Various thread dispatching protocols. 
  It can be used to compare the behaviour of Periodic, Sporadic, 
  Aperiodic, Hybrid, Timed and Background threads.

- calculator.aic: [BCS]
Integer arithmetics with the AADL Behaviour Annex. 
It can be used to show the math library capabilities 
and the interaction between the user and the simulator.

- canbus.aic: [C]
Bus communication between processors. 
It can be used to observe intercations between threads scheduling, 
and bus messages scheduling.

- coffee.aic: [BCS]
A coffee machine control system. 
It can be used to show conditional computation with the AADL Behaviour Annex.

- display_system.aic: [C]
A large model (5 processors, 13 processes and 123 threads). 
It can be used to check the scalability of the tools. 
Note that full analysis of this model can take a few minutes.

- flight_deck_door.aic: [BCS]
Access control to a flight deck door. 
This model was developed to interact with a 3D virtual reality simulation
(not provided).

- mars_pathfinder.aic: [C]
Several threads with different priority and sharing common data. 
It can be used to observe the priority inversion problem.

- multicore.aic: [C]
Partitioned scheduling on a dual-core processor. 
It can be used to practice the automatic thread placement wizard.

- pacemaker.aic: [BCS]
Ventricular pacemaker simulator.

- redundancy.aic: [BCS]
A simplistic Fault Detection Isolation and Recovery system. 
It uses the AADL Behavior Annex to detect erroneous values and 
isolate the corresponding devices.

- regulator.aic: [BCS]
A temperature regulation system. 
It can be used to illustrate the design and analysis of a 
discrete control system with the AADL Behaviour Annex.

- satellite.aic: [C]
A model defined in the AADLib github repository. 
It can be used to experiment remote model loading via the internet.

- code_generation.aic: [C]
Basic test case for Ada and C code generation with Ocarina.
Take care to only select one of the two files at a time.

- end_to_end_flow.aic: [CL]
A dataflow across a network.
Can be used for SAFLA (Scheduling Aware Flow Latency Analysis).
Thread response times are computed by the Marzhin simulator.

- lamp_examples.aic: [BCL]
Two separate models to learn about LAMP annex capabilities.
LAMP allows you to perform inline AADL model processing by adding prolog rules 
within dedicated annex subclauses and libraries.
The first example shows how to explore AADL model and annexes elements.
The second example uses output of the real-time simulation to check timing
assurance cases.

- wheel_braking_system.aic: [CE]
A model copied as is from OSATE examples base to experiment Fault Tree Analysis 
with Arbre Analyste.

- safety_security.aic: [BCELS]
A generic sensor-processing-actuator control system to highlight combined 
timing analysis (flow latency), 
safety analysis (fault tree) and 
security analysis (custom security rules).
This example was used to a illustrate paper presented during ERTS 2020 conference
https://hal.univ-brest.fr/hal-02433963/document