IST-2001-33522 OMEGA

 IAI case study

 

Case study description 

 

The main role of a Flight Control computer is to implement control loops based on computations of Command values to Servo actuators controlling the air vehicle surfaces. These computations are parameterized by the actual values provided periodically by different sensors installed in the air vehicle.

This system is critical and requires a very high reliability. For achieving this reliability, we realize the avionics system using a triple redundancy of the different Sensors and Flight Control Computers.

The software installed in the Flight Control Computer has different modules. Our case study will focus on one of them: Voting And Monitoring. The role of this module is to:

·         Provide persistent sensors values resulting of sampling 3 sensors

·         Monitor the healthiness of the sensors, based on successive comparison of sensor values

·         Monitor the healthiness of the computers, based on successive comparison of the produced command values

The environment of the “VotingAndMonitoring” module is described below.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

The actors for VotingAndMonitoring are:

·         Sensors: 3 (identical) elements providing specific information needed by the Flight Control loops: angles, velocities, accelerations, etc.

·         FC: software module, which gets sensors values and servo-actuators status as input together with commands from the Pilot or the Controlling station. It implements control loops and outputs Commands to servo-actuators

·         Channels: 2 other computers; exchange with present Computer the computed commands values

·         Health System: software module which gather information on the good operation of the avionics system and authorizes/forbids usage of the system components especially sensors and computers

·         RTC: Real-Time Clock; synchronizes the 3 computers and marks the beginning of a new computation cycle.

 

 

On the basis of this case study ,  IAI has used and done some evaluation of  3 tools :

• The Weizmann “LSC Play Engine” 
• The OFFIS “RUVE”   
• The Verimag “IF” 

 

 

Using Play Engine (Weizmann Institute) 

 

The Play Engine tool is a tool for user-friendly editing of LSC’s ( called play-in) , for the verification of consistency of LSC’s by interactive simulation (called play-out) and for synthesis of states machines from LSC’s

The IAI case study has been reduced and simplified for fitting the tool limitations and the case study version that was used on the LSC Play engine consists of one channel and three sensors .

GUI : The first stage was to define the objects of the system and to design an appropriate graphical user interface for capturing the system behavior (see below) .

Play in : Using the “Play-in” facility, the system behavior has been captured.

Play out : The “Play-out” function was activated for animating the model and  checking its behavior. RTC button is used to simulate a real-time clock time of the system and initiating a cycle model behavior. By clicking the switch, the Play-Engine identifies and displays all the LSCs that are activated by this action. If the conditions of a chart are met, the Play-Engine executes the chart; if the chart requires another user action, for example, pressing a key, the system waits for that action to be input. Each new user action may activate additional charts. As each event is executed, the GUI application reacts accordingly, showing the relevant changes

Smart Play out: For verifying the algorithm, we defined existential charts (stating a false behavior) and the smart Play out proved that this existential chart cannot be satisfied. 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

The LSC Play Engine tool was found very useful and efficient for the Play-in and Play-out functionalities. The smart play-out module was added to the Play-Engine only recently, and is therefore less robust than the rest of the Play-Engine implementation. Another of the main problems is the tool ability to handle larger systems (scalability). 

 

 

Using RUVE (OFFIS) 

 

The RUVE tool (Rhapsody UML Verification Environment) is a tool used for verification of a UML model. It is integrated into the Rhapsody environment and is based on evaluation of  “system configurations”. A system configuration is an evaluation of all the attributes of all the live objects in the system. This comprises in particular the active states of the reactive objects’ statecharts.

The main services of the RUVE are the “drive-to-state” and “drive-to-property” tasks. For these tasks, the RUVE generates a prefix of a run which leads to a system configuration with the wanted state or properties if such a run exists, otherwise it indicates that the state or property is not reachable.

This is done by checking all the possible runs of a Rhapsody design starting at the step bound -just after the initialization phase, i.e. after all objects (except for events) have been created and all reactive objects statecharts have taken the transition originating at the root state’s default state.

In order to run the tool with our case study we needed to seriously simplify the model  and reduce it to only 4 statecharts  and 12 classes  focusing in this way  on the non real time issues in the model.  We first used the RUVE for verifying that we reach some of the typical states (“Acquire”,”Done”,…) by using  “drive-to-state” services. We also used the RUVE tool for performing some verification of the voting algorithm. Namely, we checked some properties like :

-          “If for the current cycle a correct sensor is ignored, then the failures counter (monitor)   increases by one” . This property was checked by defining a new attribute to store the previous counter value and by defining a configuration in which  the difference between the counters is 1 while the sensor is correct and voting algorithm has found it “to be ignored” for this cycle  . Execution of the verification case reached indeed a system configuration satisfying the property and displayed the corresponding trace .

-          “For at least one of the correct sensors, the difference to the calculated value is less or equal to Tolerance/2 ” . This property was checked and proven in a negative way : we defined a configuration expressing the negation of the property i.e: “For any of the correct sensors, the difference to the calculated value greater than Tolerance/2” so that, the output of the verification tool should be “is not reachable”. Indeed , the execution of the verification case did not reach any system configuration satisfying the property.  

-          ….

We found the RUVE tool as a promising tool thanks to its integration within Rhapsody its reports (timing diagrams and LSC”) and its ability to define advanced un-timed verification. However , together with some modeling restrictions , it has  a serious problem of scalability (deals only with simple models) and stability.

 

 

Using  IF (Verimag) 

 

IF is a tool for verification of time-related properties and scheduling analysis. It takes into account the Omega real-time extensions and represents the UML model by a set of extended timed automata. The consistency of a model can be tested by interactive or exhaustive simulation. Properties, expressed as Omega time constraints or observers . Observers are special objects that run in parallel with a UML system and monitor its state and the events that occur. Observers are described by special UML classes stereotyped with <<observer>. They may own attributes and methods and may be created dynamically.

 

With the IF tool, we wanted to verify time related properties of our case study. In order to do so, we have modeled the timing aspects of the system with Rational Rose, as using Rhapsody posed problems with the export of the action language part and also with the timed annotations. The model used for timed verification is based on the same state machines, but the functionality (in particular the voting mechanism, including the health monitor) has been omitted ; on the other hand, all objects are active, and here we have taken into account two CPUs.

The model was extended with timed specifications :  we defined time triggered actions   and time - consuming activities of variable duration. There was no problem in exporting the model to XMI and importing it into the IF.

Case study (new) specification 

The  case study covers  3 Sensors , the  Muxbus and the  System comprising 2 CPU’s :

• The   Sensor  objects (see statechart below ) perform “idle-isFailed-acquire-sample” 50msec cycles , in which “acquire” state represents the physical measurement of the sensor  , “sample” state represents the treatment of this measurement  till the data transfer to the Muxbus and the generation of  evWrite(n) events . The randomly transition from isFailed to Ready or Acquire expresses possible  errors of the sensor
• The  Muxbus  object , receiving an evWrite event , reads the data to its memory and generates evDataReady(n) event for each one of the Nodes .
• The Node object , receiving the evDataReady(n) events , invokes  the trigger read  of Muxbus for transferring the data from Muxbus to CPU and after reception of the data values from the 3 sensors , enters the compute state in which it performs its job ( sensor voting, sensor value computation ,monitoring…)  Note that at least 2 sensors are needed for a normal operation

 

The time specifications are the following:

-          For a Sensor:

o       Acquiring of physical measurement requires  0.5 to 3 msec

o       Treatment and transfer to Muxbus requires  0.1 to  0.5 msec

-          For the Muxbus

o       Writing data from Sensor to its memory requires 100 to 200 usec

o       Reading data from its memory and provision to CPU requires  50 to 100 usec

 

Case study modeling (main statecharts)

 

Figure ‎0‑1 : Sensor Statechart

 

 

 

 

Figure ‎0‑2: Muxbus

 

 

Figure ‎0‑3 : Node (formally the System class)

 

 

 

 

 

 

 

 

 

Observers  

As an example , the following  observer (“Sampling time limits” Observer) has been defined for bounding the total time of sensor sampling  ( i.e: the time spent before the system enters computations should not be greater than 4.9 msec)

 

 

Figure ‎0‑1 : Sampling time limit observer

Other observers have been defined :

•  “Entering Error state” Observer  : This Observer checks that :  if the system has gone through error state , at most one sensor was OK . This is obtained by counting the generations of evWrite events (expressing that the sensor is OK) and by checking that in case the system has entered the error state ,  the counter value is less than 2  .
• “ Time difference” Observer : This observer evaluates (t timer) the time delay between the read of the same sensor from Muxbus memory  by two different Nodes (due to bus occupation  and checks that  this time is less than the expected limit  .

 

Summary

In order to work with the IF tool we had to remodel our case study since the tool doesn’t work with Rhapsody. We simplified the model and deleted all un-timed aspects of the model including the main algorithms – voting and monitoring. We did add a lot of timing information and made all objects active so we could explore concurrent execution.

The IF tool is impressive, has a strong capability of time analysis and model checking and it  can serve for Model debugging – simulation .Describing time properties is done by observers with statecharts. On one hand this is user friendly (statecharts), on the other hand – it can be very complex. The size of the obtained models up to three sensors and 2 CPU’s is reasonable, but when trying to add different type of sensors the size of the model explodes .

Some limitations have to be emphasized: The IF tool is not user friendly and it presents cryptic error messages. It is not connected to Rhapsody and to the other Omega tools (There are differences in semantics between IF and RUVE, for instance in the choice vertex) .In addition IF  has a big scalability problem   .