Speed up Testing and Verification

Developing large applications with hard real time requirements is often difficult. Verifying them is a real challenge.

A naïve approach is to create test cases, execute the application and examine logs/traces to verify that the system behaves as expected. But it is difficult and time consuming to define and perform these tests and to verify that the test cases cover verification of the critical run-time behavior. Multi-threading and event-driven parts of the application makes it more complex, and sometimes this complexity makes it nearly impossible to cover all possibilities.

This is where formal pre-run-time analysis comes to the rescue by enabling the user to focus on describing and modelling the application behavior including timing and resource constraints. The application can then be automatically analyzed and verified formally by formal alalysis algorithms.

Formal Modelling

The Rubus ICE (Integrated Component Development Environment) employs a simple, intuitive graphical formal modelling language to model an application, including control flow, data flow and constraints. The modelling revolves around an object called Software Circuits (a hardware analogy), corresponding to a simple function with inputs and outputs. The application is modelled by combining these building blocks.

The modelling language have been developed in collaboration with research at Mälardalens University, in close cooperation with our customers and participation in various research projects.

The Rubus models provide various viewpoints reflecting all of the necessary information concerning the development, analysis, synthesis and execution of real-time applications.

Based upon the evolution of Arcticus products, a few central concepts have evolved that drive the product related thinking as follows:

Concept-Figure-2

Formal Analysis

The formal modelling enables the powerful formal analysis methods in Rubus ICE to:

  • Create execution schedules (taking pre-emption and interrupt interference into account) that are guaranteed to hold
  • Calculate worst case response times for event trigged tasks
  • Calculate worst case stack usage
  • Calculate theoretical worst case end-to-end data delays (including several nodes communicating via networks)
  • Optimize internal data communication
  • Synthesize the application code.

By pressing “Build”, the user gets a complete application, with all constraints formally analyzed and verified by state-of-the-art algorithms.

Achieving Predictable and Dependable Systems

A key concept in Rubus is time-triggered deterministic tasks. These are scheduled pre-runtime based on their worst case execution time (and also taking interrupt interference into account). This approach results in predictable and dependable systems.