Concept

Formal Modelling
– Simple, intuitive, graphical formal modelling language.

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 has been developed in collaboration with research from 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.

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.

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 behaviour. Multi-threading and event-driven parts of the application make 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 behaviour including timing and resource constraints. The application can then be automatically analyzed and verified formally by formal analysis algorithms.

Download Rubus Tool Suite Whitepaper

Click here to download the Whitepaper outlining all the benefits and features of the Rubus Tool Suite.

Download
Scroll to Top