TIME4SYS Platform
Context
Usually, the industrial practices rely on the subjective judgment of experienced software architects and developers to predict how design decisions may impact the timing behavior of real-time embedded systems. This is however risky since eventual timing errors are only detected after implementation and integration, when the software execution can be tested on system level, under realistic conditions. At this stage, timing errors may be very costly and time consuming to correct. Therefore, to overcome this problem there is a need for efficient, reliable and automated timing estimation methods applicable already at early design stages and continuing throughout the whole development cycle.
Introducing timing verification activities into the design process of real-time embedded systems has always been a challenge as the inputs required for the verification, in particular the worst-case execution time and the system behavior description, are moving target all across the different design phases. Thanks to the introduction of model based methods (in particular viewpoints for non-functional properties) in the industrial development process [4], this goal seems to be reachable for model-based verification techniques, such as simulation, scheduling analysis or model-checking. Starting from very high level system architecture and rough timing allocations, the model-based timing verification has to be refined at each step of the project (architectural design, detailed design, coding, unit test and software validation phases) down to concrete timing measurements on the final system. A major problem however persists: model-based timing verification techniques are often not directly applicable to conceptual design due to the semantic gaps between their respective models. Solving this issue is essential to break the remaining walls separating model-based timing verification from the development process of real-time embedded systems, and to enable its use in the industry.
PolarSys Time4Sys
PolarSys Time4Sys is a timing performance framework that fills the semantic gaps between the design models of real-time systems and the models of timing verification tools. Time4Sys is composed of two building blocks (the Design and the Verification pivot models) as well as a set of transformation rules between them. Both pivot models are based on the Time4Sys meta-model.
Time4Sys uses a subset of the MARTE OMG standard [7] as a basis to represent a synthetic view of the system design model that captures all elements, data and properties impacting the system timing behavior and required to perform timing verification (e.g. tasks mapping on processors, communication links, execution times, scheduling parameters, etc.). Time4Sys is not limited to the use of a particular design modeling tool and environment. It can be connected to various environments and languages such as UML, SysML [6], AADL [5], or any other proprietary environment (e.g. Capella).
Figure 1: Bridging the gap between design tools and verification tools
Scheduling analysis and simulation are seldom directly applicable to the conceptual design models in general and to Time4Sys Design models in particular due to the semantic mismatch between the latter and the variety of analysis and simulation models known from the classical real time systems research and represented by academic and commercial tools. Transformation rules are therefore required to generate a Time4Sys Verification model preserving the timing behavior modeled in the corresponding Time4Sys Design model, while ensuring the compatibility with the variety of existing timing verification tools. After timing verification in the selected tool, results are injected in Time4Sys Verification model. Then, they are translated to be compliant with the original design model and injected back in Time4Sys Design.
Time4Sys Architecture
By using MDE settings, Time4Sys is being developed as an Eclipse Polarsys plugin. Time4Sys proposes four capabilities: modeling and viewing the Time4sys model, A dedicated meta-model based on the MARTE standard (available for download), model transformations able to transform and adapt Time4sys model for verifications tool and connectors to import/export models from design tools and verifications tools.
Figure 2: Time4Sys Platform architecture
Time4Sys meta-models:
The Time4Sys framework is composed by 4 Meta-models:
- The MARTE meta-model which implement the MARTE standard Language to capture all concepts related to model real-time software and embedded hardware.
- The Design Meta-model which extends the MARTE meta-model with missing concepts need to model the design model of the application and to model the verification model.
- The Results meta-model contains all concepts required to model various results produced by verification tools and need to be provided to the design architects.
- The Trace Meta-model contains concepts to model traces to model Gantt charts and execution traces.
Time4Sys graphical editor:
The graphical editor for the Time4Sys models is a java module based on Sirius [8]. It offers the capabilities to edit and view Time4Sys models via a graphical user interface. This module also offers menus to apply model transformations rules and launch the appropriate verification tool (Pegase [3], MAST [1], Cheddar [2] and in the future ROMEO [9]). The next Figure shows the graphical interface for this editor.
Figure 3: Time4sys model editor
Time4sys model transformations rules:
The transformations rules aim to transform Time4sys model into another time4sys model by solving semantic gaps for verification tools. Time4sys proposes a set of transformations rules which can be assembled together to solve the semantic gaps between design models and verification tool models.
Time4sys connectors:
A connector is able to bridge the Time4sys framework to a design tool, a verification tool or a visualization tool. Time4sys is provided with connectors able to import/export Time4sys model to Pegase Tool [3], MAST [1] and Cheddar [2] (ongoing). ROMEO [9] connector is currently in under study. A prototype of the connector to the design tool Capella [10] will be also provided.
Note: The MARTE meta-model can be downloaded as a separate and independent package. Time4sys aims to be the official repository for the MARTE meta-model.
System documentation:
Available at https://polarsys.org/time4sys/documentation/
References
[1] MAST, “Modeling and analysis suite for real-time applications,”http://mast.unican.es/
[2] “The cheddar project: a gpl real-time scheduling analyzer,” http://beru.univ-brest.fr/ singhoff/cheddar/
[3] RTaW-Pegase, “Modeling, simulation, and timing analysis for communication networks,” http://www.realtimeatwork.com/software/rtawpegase/.
[4] K. Balasubramanian, A. S. Krishna, E. Turkay, J. Balasubramanian, J. Parsons, A. S. Gokhale, and D. C. Schmidt, “Applying model-driven development to distributed real-time and embedded avionics systems,” IJES, vol. 2, no. 3/4, pp. 142–155, 2006.
[5] AADL, “Architecture analysis and design language,” http://www.aadl.info/aadl/currentsite/
[6] SysML, “Systems modeling language,” http://www.omg.org/spec/SysML
[7] MARTE, “Modeling and analysis of real-time and embedded systems,” http://www.omg.org/omgmarte/
[8] SIRIUS, Sirius enables the specification of a modeling workbench in terms of graphical, table or tree editors with validation rules and actions using declarative descriptions. https://www.polarsys.org/eclipse/sirius
[9] ROMEO, D. Lime, O. H. Roux, C. Seidner, and L.-M. Traonouez. Romeo: A parametric model-checker for Petri nets with stopwatches. In TACAS, volume 5505 of Lecture Notes in Computer Science, pages 54–57. Springer, 2009. http://romeo.rts-software.org/
[10] CAPELLA: a model-based system engineering tool and methodology, https://polarsys.org/capella/
