NLR case study description

 

The case study involves the Medium Altitude Reconnaissance System (MARS) deployed by the Royal Netherlands Air Force on the F-16 aircraft. The system employs two cameras to capture high-resolution images. The MARS counteracts the image quality degradation caused by the forward motion of an aircraft by creating a compensating motion of the film during the film exposure. The controls applied to the camera for the film speed of the Forward Motion Compensation (FMC) and the Frame Rate are being computed real-time based on the current aircraft altitude, ground speed, and some additional parameters. The system is also responsible for producing the frame annotation containing time and the aircraft’s current position, which must be synchronised with the film motion. The system also performs health monitoring and alarm processing functions.

 

Schematic representation of the MARS

 

The MARS software is responsible for the following system functions:

• Camera and film exposure control:
• Frame Rate of the film exposures
• Aircraft Forward Motion Compensation during the film exposure
• Film annotation, per frame, with the following data:
• Latitude of the current aircraft position
• Longitude of the current aircraft position
• Time of day
• System health monitoring
• Alarm processing

 

Camera and film exposure control

 

In order to perform the camera and film-exposure control functions system acquires the current altitude and velocity data from the avionics data bus of the aircraft. Based on these values it computes the film Frame Rate to be used and the value for the Forward Motion Compensation (FMC) signal. The computed values are sent to the Trigger & Exposure Module via a serial link. When pilot depresses the camera trigger button, the Trigger & Exposure Module generates the trigger pulses (with the computed Frame Rate) and applies the computed FMC signal to the film transport control of the camera.

 

Film annotation

 

In order to perform the film annotation functions system acquires the current navigation data (latitude, longitude and heading) as well as time-of-day value from the avionics data bus of the aircraft. It formats the data and sends it to the Annotation Module via the serial link. After the completion of each frame exposure cycle the camera halts the film and issues an annotation request to the Annotation Module. Upon reception of this request the Annotation Module provides the current annotation data to the camera via a serial link. After the reception of the annotation data the camera annotates current frame. The annotation cycle must be completed before the next frame exposure cycle begins.

 

Health monitoring and alarm processing

 

In order to perform the system health monitoring and alarm processing functions system processes the operational status of the various MARS components (e.g. camera status, serial communication status, data bus status, statuses of the hardware modules, etc.) and generates pilot alarms according to the alarm processing logic.

 

System properties

 

The following system properties characterise the subject of the case study:

·        The deadline on response to the annotation data request from the cameras, which also includes the data transfer time;

·        Hard timing requirement on the age of annotation data supplied to the camera, which includes the total data processing time from acquisition to proper formatting;

·        Hard timing requirement on the age of data used for the exposure control, which includes the total data processing time from acquisition to generation of the control signals;

·        Hard timing requirements on the data acquisition and processing time in order to accommodate the data rate of the avionics data bus.

The system performs asynchronous data acquisition from the avionics data bus, while performing concurrent cyclical internal processing with several different cycle times:

·        Data processing;

·        Data transfer to the annotation and trigger & exposure modules via the serial link;

·        Health monitoring and alarm processing;

·        Control Panel display update;

·        Control Panel commands processing.

 

Environment constraints and properties

 

Environment’s non-deterministic nature with its influence on the system operation is in the centre of the case study. The following constraints and properties of the environment played major role in the case study:

• Data sources provide data with the 25 ms cycle and a jitter of ±5 ms
• The data sources are independent and are not synchronised
• The data messages may occasionally be lost due to the transmission errors
• The Data-bus Controller may exhibit built-in-test errors
• The Annotation and Trigger & Exposure modules are connected to the main RCU module via one serial port

 

 

Modelling and verification examples

 

High-level requirements modelling

Untimed modelling and verification

Timed modelling and verification

 

 

High-level requirements modelling

 

The high-level requirements modelling is performed with the use of LSCs and the PlayEngine tool. The LSC model is based on the subset of the software system requirements of the MARS case study. The following activities have been represented:

• Data generated by the external sources and provided to the system
• High-level data acquisition activities
• High-level data processing activities and data transfer to the external control modules.

The model is time-driven and contains some timing constraints specifications derived from the requirements. Below are examples of the case study LSC model.

 

LSC of the Navigation data source

 

LSC of the data processing

 

Next to the LSC modelling several verification experiments have been performed on the developed model using the model verification facility provided by the PlayEngine tool, which makes use of the SMV model checker. Below are some property LSC specifications used in the verification experiments.

 

Property: If a Navigation data message has been acquired by the BusController, the RCU (Main Module) will eventually transfer the new Annotation data to the AnnotationModule and Exposure data to the ExposureModule

 

 

Property: If an Altitude data message has been acquired by the BusController, the RCU (Main Module) will transfer the new Exposure data to the ExposureModule at most 70 time units later

 

 

Untimed modelling and verification

 

Untimed UML modelling is performed with the use of Rhapsody tool from I-Logix. For the purpose of untimed verification experiments the UML Verification Environment (UVE) tool from OFFIS is being applied to the data acquisition part of the MARS model. The UVE tool provides facilities for untimed model checking of UML models. Property specification in the UVE tool is based on propositional logic and temporal logic patterns. The case study model is event-driven with non-deterministic external event trace being used to drive the behaviour of the environment. To provide for environment’s liveness and to restrict its full non-determinism the temporal logic-based assumptions are used. Some examples of the case study UML modelling are given below.

 

Air data acquisition class diagram