Osate 2 Lute

From AadlWiki

Jump to: navigation, search

OSATE2 includes Lute, a constraint language developed by Rockwell Collins. Lute is also a refinement of REAL, a constraint language initially implemented in Ocarina.

Contents

Installing Lute

If you are planning to use the latest sources, grab them from the osate2-plugins repository under the develop branch. See https://github.com/osate/osate2-plugins/tree/develop


Language definition

Rationale

Lute is a language to query AADL models and help designer to check model structure and system requirements. It is composed of different functions to query the components hierarchy as well as their characteristics (features, connections, etc.) and properties. The first version of such language was REAL, developed by Olivier Gilles in the Ocarina toolsuite.

Lute is initially developed by Rockwell Collins and is now integrated within OSATE as an officially supported plug-in.

Language structure

The language uses a theorem approach with a notation similar to mathematics. You can browse the component hierarchy using the foreach statement and define set. A set is a list of unordered components or values. The languages defines a predefined collection of sets and users can define their own.

Let's consider the following example :

 theorem Memories_Properties
    foreach s in System_Set do
       foreach mainmem in {m in Memory_Set | Is_Direct_Subcomponent_Of (m, s)} do
           check (Property_Exists (mainmem,"Byte_Count"));
 end;

In the following, we browse the System_Set predefined set that contains all system components. Then, for each system component, we build a new set that contains all memory components contained in the system component under analysis. Then, for each memory component of this set, we check that the property Byte_Count is defined.

Predefined sets

  • System_Set
  • Data_Set
  • Thread_Set
  • Process_Set
  • Memory_Set
  • Processor_Set
  • Bus_Set
  • Virtual_Bus_Set
  • Virtual_Processor_Set
  • Device_Set
  • Connection_Set


Language functions

  • Property: retrieve the value of a property
  • Property_Exists: returns a boolean indicating if a property exists on a component
  • Is_Bound_To: returns true is a component is bound to another one. For example, a process bound to a processor or a memory.
  • Source: source of a connection
  • Destination: destination of a connection
  • Member: returns true if a value is within a set
  • Owner: return true if a component is the owner of another (containment relation, one component containing another)
  • Is_Subcomponent_Of: returns true if a component is a subcomponent of another or its owners (search recursively the owner)
  • Is_Direct_Subcomponent_Of: returns true if a component is a subcomponent of another one but does not look recursively
  • Is_Type_Of: returns true is the type of the first argument (AADL component) contains the string of the second argument</li>
  • Sum: result of adding all the elements of a set
  • Max: maximum value of a set
  • Min: minimum value of a set
  • Cardinal: number of elements in a set
  • Lower: lower value of a range
  • Upper: upper value within a range


Query the model

Lute comes with a dedicated menu that proposes different options :

  • Use the theorems from META, a project from Rockwell-Collins. This is a predefined set of theorems
  • Use your own file that contains your theorems
  • Use the Lute console to design your own theorem

To run Lute on your model, select the system implementation of your root system instance in the outline view and then, select the Lute menu as shown in this picture.


The Lute console

Lute comes with its own console to help you editing your theorem. You can write your own theorem (as shown in this picture) or just pick one predefined theorem in the list (and potentially improve/refine it), as shown in this picture.


Theorem examples

Process binding

The following check that each process is bound to a processor and a memory.

 theorem Partitions_Bindings
  foreach prs in Process_Set do
        segments := {x in Memory_Set | Is_Bound_To (prs, x)};
        runtimes := {y in Processor_Set | Is_Bound_To (prs, y)};
  
        check ( (Cardinal (segments) = 1 ) and (Cardinal (runtimes) = 1 ));
 end;

Process memory

The following process check that for each process, the memory required by the thread can be provided by the memory component associated with the process.

 theorem check_memory_requirements_partitions
  foreach prs in Process_Set do
     Thrs := {x in Thread_Set | Is_Direct_Subcomponent_Of (x, prs)};
     mems := {x in Memory_Set | Is_Bound_To (prs, x)};
     check
        ((Sum (Property (Thrs, "Source_Stack_Size")) + Sum (Property (Thrs, "Source_Data_Size")) + Sum (Property (Thrs, "Source_Code_Size")))
           < (Sum (Property (mems, "byte_count")))
        );
 end;

Criticality

The following theorem checks that two connected partitions have the same criticality level. The criticality level is defined on the virtual processor bound to each process.

 theorem safety
 foreach Conn in Connection_Set do
    foreach P_Src in {x in Process_Set | Owner (Source(Conn)) = x} do
      foreach P_Dst in {y in Process_Set | Owner (Destination(Conn)) = y} do
      foreach Runtime_Src  in {w in Virtual_Processor_Set | Is_Bound_To (P_Src, w)} do
        foreach Runtime_Dst  in {z in Virtual_Processor_Set | Is_Bound_To (P_Dst, z)} do
            check ( (Property (Runtime_Src, "ARINC653::Criticality")) = (Property (Runtime_Dst, "ARINC653::Criticality")));
 end;


Use of Is_Type_Of

 theorem checkfamily
 foreach p in { element in Processor_Set | Is_Of_Type (element, "e500mc")}
 do
    check Property_Exists (p, "Processor_Properties::Processor_Family");
 end;

Help & Support

If you have any issue and problem to report, please fill a bug report and/or contact us on the AADL users mailing-list.

Personal tools