Perform Formal Verification

Formal verification methods in DANSE are still under development. In this deliverable we start documenting the methods used to perform timing analysis of the system. Future versions of this deliverable will include additional methods for formal verification.

Description

Whenever timing constraints are annotated to constituent system models or parts of these, or to the SoS itself, the behaviors of the corresponding CSs have to be validated against these constraints. Especially for safety critical functions and services such timing constraints have to be validated. Timing plays a major role when different constituent systems cooperate, e.g. when some CSs expect that their required services are delivered within a specific time frame with respect to their request.

Initial Situation

For our analysis approach, the available SoS/CS model, which should be analyzed, has to contain some specific timing information:

  • Deadlines are annotated with the aid of the GCSL. Timing constraints have the following syntax:

whenever a occurs b occurs within [lb, ub]

Here a and b are observable events such as requests for services sent between different constituent systems, and [lb, ub] specifies the time frame, which is allowed to pass between both events.

Deadlines can specify both global (i.e. deadlines concerning a set of CS) and local deadlines (timing requirements within a specific constituent system).

  • All relevant elements of the considered architecture are annotated with timing specific information:
    • On each constituent system a set of services or functions has to be allocated.
    • Services and sequences of functions describing the behavioral part of the architecture are annotated with execution times. These execution times specify the durations between calling the function until the termination without considering interruptions (which would increase the execution times). Further, services are annotated with priorities, such that these can be interrupted, when a more critical service is needed to be performed.
    • Independent services, i.e. services, which do not depend on the output of some other services, are periodically triggered by event streams
    • Each constituent system has a so called scheduling policy determining the execution sequence of all allocated services.

It is assumed, that for the timing annotations the MARTE profile is used.

The state spaces of the CS are then computed iteratively. For this, we use abstraction and composition operations in order to keep the state spaces as small as possible. With the choice of the concrete abstraction operation we are able to trade off the accuracy of the response times while affecting the needed state spaces.

Expected Result

When the timing analysis is called for (a part of) an SoS architecture, it will deliver the information whether all timing properties are met. In case of a violation of a requirement a counter example will be returned.

Required Tools

  • Rhapsody
  • UPDM 2.0
  • DANSE Profile Extension for Rhapsody
  • DANSE Profile Extension with MARTE annotations
  • DBM Library from Uppaal

 

Figure 57. Tool Flow: Perform Formal Verification

Activities

  • Model SoS: All necessary constituent systems inter-connections are specified. For this, the allocated functions/services which are executed on some resources of the corresponding CS are captured, and dependencies between functions are modelled.
  • Specify timing properties: Add timing relevant information to the services, i.e. execution times and priorities
  • Add Scheduling information to each resource of each CS
  • Specify timing requirements: Add local and global timing constraints
  • Export model to RTANA (timing analysis tool, this is work in progress)
  • Execute RTANA
  • If all constraints are met, then nothing needs to be changed
  • Else if at least one constraint is violated, appropriately adapt the model


 

Figure 58 Activity diagram for checking timing properties

Limitations

  • Timing properties are available and modelled via Marte-Profile
  • Independent services are periodically triggered
  • Dependencies between services are captured, i.e. corresponding resources or CSs are connected
  • There are no cyclic dependencies

Follow-up Solution Methods

  • Generate optimized architectures: determine the performance of the current architecture and find "better" ones (wrt. to the used metrics)
  • Generate architecture alternatives: if some timing properties are violated, adapt the architecture in an appropriate way
Home About Technical Approach Perform formal verification