Time4sys2imi: A tool to formalize real-time system models under uncertainty

TL;DR

Time4sys2imi is a tool that translates graphical real-time system models into formal automata, enabling schedulability analysis and timing constraint inference under uncertainty.

Contribution

It introduces a translation from Time4sys to parametric timed automata, facilitating formal analysis of real-time systems.

Findings

Successful application to various examples

Enables schedulability checking and timing constraint inference

Bridges graphical models with formal verification tools

Abstract

Time4sys is a formalism developed by Thales, realizing a graphical specification for real-time systems. However, this formalism does not allow to perform formal analyses for real-time systems. So a translation of this tool to a formalism equipped with a formal semantics is needed. We present here Time4sys2imi, a tool translating Time4sys models into parametric timed automata in the input language of IMITATOR. This translation allows not only to check the schedulability of real-time systems, but also to infer some timing constraints (e.g., deadlines, offsets) guaranteeing schedulability. We successfully applied Time4sys2imi to various examples.

Tables

Table 1. Table 1 : Summary of experiments

Case study	Example 1[Fig. 1]		Example 2 [Fig. 5]		Example 3 [Fig. 7]		Example 4 [Fig. 10]
# CPU	2		1		1		4
# tasks	4		4		3		11
# tasks chains	2		0		1		4
# number of automata	6		9		3		12
# total number of locations	22		26		14		53
# clocks	8		8		6		22
# discrete	4		4		3		11
# parameters	0	2	0	1	0	2	0	3
Parameters	-	WCETStep1	-	DeadlineStep2	-	DeadlineStep1	-	WCETStep5
		BCETStep1						BCETStep5
								DealineStep11
Execution time (seconds)	0.040	0.112	0.263	0.289	0.042	0.045	2.276	144.627
Schedulable?	$\times$	Condition1	$\surd$	Condition2	$\surd$	Condition3	$\surd$	Condition4

Table 2. Table 2 : Synthesized constraints

Condition1	Condition2	Condition3	Condition4
5 $>$ WCETStep1	DeadlineStep2 $>=$ 4	DeadlineStep1 $>=$ 5	WCETStep5 $>=$ BCETStep5
& BCETStep1 $>=$ 0			& BCETStep5 $>=$ 0
& WCETStep1 $>=$ BCETStep1			& 15 $>$ WCETStep5
			& DeadlineStep11 $>=$ 5
			OR
			5 $>$ DeadlineStep11
			& BCETStep5 $>$ 4
			& DeadlineStep11 $>=$ 2
			& WCETStep5 $>=$ BCETStep5
			& 6 $>=$ WCETStep5
			OR
			DeadlineStep11 $>=$ 2
			& 5 $>$ DeadlineStep11
			& 15 $>$ WCETStep5
			& BCETStep5 $>$ 14
			& WCETStep5 $>=$ BCETStep5

Full text

linecolor=red,backgroundcolor=red!25,bordercolor=red]Instructions: ICTAC 2019: Short and tool papers should not exceed 10 pages.

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: hello linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]JJ: hello

1 Introduction

Due to the increasing complexity in real-time systems, designing and analyzing such systems is an important challenge, especially for safety-critical real-time systems, for which the correctness is crucial. The scheduling problem for real-time systems consists in deciding which task the processor runs at each moment by taking into consideration the needs of urgency, importance and reactivity in the execution of the tasks. Systems can feature one processor (“uniprocessor”) or several processors (“multiprocessor”). Each processor features a scheduling policy, according to which it schedules new task instances. Tasks are usually characterized by a best and worst case execution times (BCET and WCET), and are assigned a deadline and often a priority. Tasks can be activated periodically (“periodic task”), sporadically (“sporadic tasks”), or be activated upon completion of another task—to which we refer to “dependency” or “task chain”. This latter feature is often harder to encode using traditional scheduling models. Periodic tasks may be subject to a “jitter”, i. e., a variation in the period; all tasks can be subject to an “offset”, i. e., a constant time from the system start to the first activation of the task. The schedulability problem consists in verifying that all tasks can finish their computation before their relative deadline, for a given scheduling policy. This problem is a very delicate task: The origin of complexity arises from a large number of parameters to consider (BCET and WCET, tasks priorities, deadlines, periodic and sporadic tasks, tasks chains, etc.). The schedulability problem becomes even more complicated when periods, deadlines or execution times become uncertain or completely unknown: we refer to this problem as schedulability under uncertainty.

Thales Group, a large multinational company specialized in aerospace, defense, transportation and security, developed a graphical formalism Time4sys111https://github.com/polarsys/time4sys to allow interoperability between timed verification tools. Time4sys responds to a need to unify the approaches within Thales Group: This formalism is being rolled out at TSA (Thales Airborne Systems) and studies are underway at TAS (Thales Alenia Space). Time4sys is now an open source framework, offering many features to represent real-time systems. However, Time4sys lacks for a formalization: it does not perform any verification nor simulation, nor can it assess the schedulability of the depicted systems.

Since Time4sys does not allow to perform formal analyzes for real-time systems, a translation to a well-grounded formalism is needed to verify and analyze real-time systems. In this paper, we present a tool Time4sys2imi which allows to translate Time4sys into parametric timed automata (PTAs) [AHV93] described in the input language of IMITATOR. PTAs extend finite-state automata with clocks (i. e., real-valued variables evolving at the same rate) and parameters (unknown timing constants). PTAs are a formalism well-suited to verify systems where some timing delays are known with uncertainty, or completely unknown. IMITATOR [And+12] is the de-facto standard tool to analyze models represented using PTAs. This translation allows not only to assess the schedulability of systems modeled using Time4sys, but only to synthesize some timing constants guaranteeing schedulability.

In [And19], we presented a set of rules translating Time4sys to PTAs. We introduce here the tool performing this translation, with its practical description, as well as a set of case studies, absent from [And19].

Related works

Scheduling using (extensions) of timed automata was proposed in the past (e. g., [AAM06]). For uniprocessor real-time systems only, (parametric) task automata offer a more compact representation than (parametric) timed automata [Fer+07, NWY99, And17]; however [Fer+07, NWY99] do not offer an automated translation and, while [And17] comes with a script translating some parametric task automata to parametric timed automata, the case of multiprocessor is not addressed. Schedulability analysis under uncertainty was also tackled in the past, e. g., in [CPR08, Fri+12, Sun+13].linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: Todo after acceptance of this paper: add Ariane paper The main difference with our tool is that we allow here a systematic translation from an industrial formalism.

An export from Time4sys is available to Cheddar [Sin+04]. However, while Cheddar is able to deduce schedulability of real-time systems, it suffers from two main limitations:

it does not allow task dependencies; and 2. 2.

all timing constants must be fixed in order to study the schedulability.

In contrast, our translation in Time4sys2imi allows for both.

A model represented with Time4sys can also be exported to MAST [Gon+01] which is an open-source suite of tools to perform schedulability analysis of real-time distributed systems. However, the effectiveness of this tool is limited: it does not allow us to have a complete solution to our problem since it only works with instantiated systems, so we can not perform a real-time system with unknown parameters.

Outline

Section 2 describes Time4sys, and states the problem. Section 3 exposes the architecture of Time4sys2imi. As a proof of concept, Section 4 gives the results obtained on some examples. We discuss future works in Section 5.

2 Time4sys in a nutshell

We review here Time4sys, and make a few (minor) assumptions to ease our translation.

Time4sys is a formalism that provides an environment to prepare the design phase of a system through the graphical visualization developed. Time4sys contains two modes: Design and Analysis. In our translation, we use the Time4sys Design mode which uses a subset of the OMG MARTE standard [OMG08] as a basis for displaying a synthetic view to the real-time system. This graphical representation encompasses all the elements and properties that can define a real-time system.

The Time4sys Design tool allows users to define the following elements:

• •

Hardware Resource: a hardware resource in Time4sys is a processor, and it contains a set of tasks; it is also assigned a scheduling policy.

• •

Software Resource: a software resource in Time4sys is a task, and it features a (relative) deadline.

• •

Execution Step: an execution step can be seen as a subtask. It is characterized by a BCET, a WCET, and a priority. In our translation, we assume that each software resource contains exactly one execution step. That is, we do not encompass for subtasks.

• •

Event: an event can be seen as an activation policy for tasks. There are two main types of Events:

• –

PeriodicEvent: defined by its period, its jitter and its phase (i. e., offset).

• –

SporadicEvent: defined by its minimum and maximum interarrival times, its jitter and its phase.

Example 1

Fig. 1 shows an example of a real-time system designed with Time4sys. In this example, we have two hardware resources (HardwareResource0, HardwareResource1) both using fixed priority as a scheduling policy, two software resources (SoftwareResource1, SoftwareResource2) in each hardware resource, and four execution tasks, with the following timing constraints:

• •

Step1: $\mathit{WCET}=\mathit{BCET}=6\,ps$

• •

Step2: $\mathit{WCET}=\mathit{BCET}=4\,ps$

• •

Step3: $\mathit{WCET}=\mathit{BCET}=5\,ps$

• •

Step4: $\mathit{WCET}=\mathit{BCET}=5\,ps$

Finally, this example features two periodic events, both characterized by a 10 ps period, a 0 ps jitter and a 0 ps phase (“offset”). linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: il manque la priorité des tâches

In this example, we start executing with Step1 in the CPU HardwareResource0. After 6 ps, the execution of Step1 ends so Step2 takes its place. At the same time, Step3 in the CPU HardwareResource1 starts performing. At $t=10\,ps$, the execution of Step2 finishes and a new period of Step1 starts, however at that time Step3 is still executing. So this real-time system is not schedulable i. e., the period of StepT1 is strictly less than the WCET of Step1 plus the WCET of Step3.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: ça manque un peu d’explications, en fait

Time4sys Design can be used for different design modeling tool. It can be exported to different languages such as UML and AADL.

Objective

The main objective of Time4sys2imi is as follows: given a real-time system with some unknown timing constants (period, jitter, deadlines…), synthesize the timing constants for which the system is schedulable. Note that, when all timing constants are known precisely, this problem is schedulability analysis.

3 Architecture and principle

The main purpose of Time4sys2imi is to perform the translation of Time4sys models into the input language of IMITATOR. The schedulability analysis itself is done by IMITATOR, using reachability synthesis.

3.1 Targeted user

The application is intended primarily for the designer of real-time systems, aiming to verify the schedulability of her/his system, or synthesize the timing constants ensuring schedulability.

Time4sys2imi can automatically analyze a graphical representation of a real-time system realized by Time4sys using IMITATOR. The end-user does not need to have skills on PTAs nor on model checking.

Time4sys2imi allows the user to:

• •

Use the GUI of Time4sys2imi (cf. Fig. 2) and configure the options of both the translation and IMITATOR.

• •

Import an XML file generated by Time4sys. This file contains the data that describes the real-time system to be analyzed.

• •

Generate an .imi model analyzable by IMITATOR.

3.2 User workflow

The analysis of real-time systems, using the proposed translation, can be summed up in three main parts:

Graphical modeling of a real-time system containing all its components with Time4sys. This part allows us to have a complete architecture of the system on the one hand. The architecture is encoded in an XML file automatically generated by Time4sys. This file contains all the data needed to describe the system. 2. 2.

The second part is the automatic translation of the XML file to the input language of IMITATOR, and is performed by Time4sys2imi. Time4sys2imi creates an .imi file that is analyzable with IMITATOR. 3. 3.

Finally, the user can run IMITATOR from Time4sys2imi to get the answer to the schedulability problem. linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: mais est-ce que tout est intégré, ou est-ce que l’utilisateur doit lui-même exécuter IMITATOR ?

The translation rules are described in [And19]. In short, we translate each task, each task chain and each processor scheduling policy (earliest deadline first, rate monotonic, shortest job first…) into a PTA; most of these PTAs feature a special location corresponding to a deadline miss (i. e., this location is reachable iff a deadline miss occurs). Timing constants are encoded either as constants (if they are known) or as timing parameters (if they are unknown). Then, we build (on-the-fly) the synchronous product of these PTAs. Finally, the set of valuations for which the system is schedulable is exactly those for which the special deadline miss locations in the synchronous product are unreachable. See [And19] for details.

3.3 Global architecture

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: mais il manque des infos essentielles ici : quel est le langage de programmation de Time4sys2imi ? Combien de lignes de code ? Quel système d’exploitation peut-on utiliser pour son utilisation ? Est-ce que tout est intégré ensemble (time4sys + traduction + IMITATOR ou faut-il faire plusieurs étapes ? etc.

Time4sys2imi is made of 5,500 lines of Java code, and can therefore run under any operating system. We explain in Fig. 3 the global architecture of the system. linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: ok, mais je vois pas bien les 3 parties sur la Fig. 3 ; on a l’impression que ta figure (qui est intéressante quand même) ne correspond pas bien au texte.

Time4sys2imi takes as input the Time4sys model in XML, then we used the DOM parser to extract data. These data are translated into an abstract syntax for PTAs. We then translate these abstract PTAs into the concrete input language of IMITATOR.

3.4 Detailed architecture

The global process is in Fig. 4.

Level 1

This level is the interface between the translation tool and the user: It allows the user to import the XML file to be translated, to choose the name of the IMITATOR model and to confirm the translation request.

Level 2

This level is loaded by the translation of the XML file through the following steps:

1. 1.

Parsing the XML file that Time4sys generates in order to get an abstract data structure from Time4sys. 2. 2.

Translation of the result into an abstract data structure of PTAs. 3. 3.

Construct an IMITATOR file from the PTAs abstract data structure.

Level 3

This level shows the XML files generated by Time4sys when designing a real-time system.

4 Proof of concept

As a proof of concept to show the applicability of our translation tool, we modeled some real-time systems with Time4sys, then we translated those models to PTAs using with Time4sys2imi and analyzed them using IMITATOR.

We give in Table 1 a list of four case studies with, from top to bottom, the number of CPU, of tasks and task chains in the original Time4sys model, followed by the number of automata, locations, clocks, discrete variables222Discrete variables are global rational-valued variables that can be read and modified by the PTAs. and parameters in the translated IMITATOR target model. We also give the name of the constants that are indeed parameterized (if any), and give the analysis time by IMITATOR. The translation time using Time4sys2imi is always negligible in our experiments.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: tu n’as pas un ordre de grandeur, tout de même ? Finally, we give whether the system is schedulable (if it is entirely non-parametric), or we give the condition for which it is schedulable. The parametric results (i. e., the constraints over the valuations ensuring schedulability) are given in Table 2 in Section 0.A.5.

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: dans Table 1, j’aurais aimé voir le nombre d’automates, et de locations (si tu as gardé les données) ; tu peux ajouter ?

We ran experiments on an ASUS X411UN Intel Core$\texttrademark$ i7-8550U 1.80 GHz with 8 GiB memory running Linux Mint 19 64 bits. All experiments were conducted using IMITATOR 2.10.4 “Butter Jellyfish”.

Source, binaries, examples and results are available at www.imitator.fr/static/ICTAC19.

From Table 1, we see that the analysis time using IMITATOR remains small, with the exception of the larger model with 11 concurrent tasks featuring dependencies, for which the analysis time using IMITATOR for a three-dimensional analysis becomes above 2 minutes.

Example 2

Consider again the real-time system modeled in Fig. 1 using Time4sys. We translate it using Time4sys2imi; the set of PTA obtained for this example are illustrated in Fig. 9 in Appendix 0.A.

First, we consider a non-parametric analysis: applying IMITATOR to the PTAs translated using Time4sys2imi shows that the system is not schedulable, as it was expected from Example 1.

Second, we parameterize the BCET and WCET of Step1. The result of the schedulability synthesis using IMITATOR yields the following constraint: $0\leq\mathit{BCETStep1}\leq\mathit{WCETStep1}<5$.

This constraint explains why this real-time system was not schedulable when $\mathit{WCET}=\mathit{BCET}=6$ i. e., the values taken for $\mathit{WCET}$ and $\mathit{BCET}$ are not in the interval for which the system is schedulable.

Additional examples with models and translated PTAs are given in Appendix 0.A.

5 Perspectives

A short term future work will be to optimize our translation: while we followed the rules developed in [And19], it is likely that varying the rules in order to optimize the size of the automata or reducing the clocks, may help to make the model more compact and the analysis more efficient.

Second, when the model is entirely non-parametric, we believe that using the Uppaal model checker [LPY97] instead of IMITATOR may be more efficient; for that purpose, we plan to develop a translator to the input language of Uppaal too; this implies to modify only the last step of our translation (from the abstract (P)TAs into the concrete input language of the target model checker).

Third, so far the analysis using IMITATOR is exact, i. e., sound and complete; however, it may sometimes be interesting to get only some ranges of parameter valuations for which the system is schedulable. Such optimizations (on the IMITATOR side) should help to make the analysis faster.

Seeing from our experiments, it is unlikely that the toolkit made of Time4sys, Time4sys2imi and IMITATOR can analyze models with hundreds of processors and thousands of tasks, especially with unknown timing constants. However, we believe that our approach can give first useful guarantees at the preliminary stage of system design and verification, notably to help designers to exhibit suitable ranges of timing parameters guaranteeing schedulability. Finally, real-time systems with uncertain timing constants were recently proved useful when Thales Group published an open challenge333“Formal Methods for Timing Verification Challenge”, in the WATERS workshop: http://waters2015.inria.fr/challenge/ for a system (actually modeled using Time4sys) with periods known with a limited precision only; while this problem was not strictly speaking a schedulability problem (but rather a computation of minimum/maximum execution times), it shed light on the practical need for methods to formally analyze real-time systems under uncertainty in the industry.

Acknowledgements

We thank Romain Soulat and Laurent Rioux from Thales R&D for useful help concerning Time4sys.

This work is partially supported by the ASTREI project funded by the Paris Île-de-France Region.

Appendix 0.A Additional details on the experiments

0.A.1 Example without tasks chain

We modeled an example with Time4sys presented in Fig. 5. This example contains four periodic tasks without task chains.

Fig. 6 illustrates the PTAs obtained from Fig. 5 after the translation using Time4sys2imi. This graphics is automatically generated by IMITATOR (as the subsequent PTA depictions).

0.A.2 Example with tasks chain

We modeled an example with Time4sys presented in Fig. 7. This example contains three tasks, of which one is periodic; it contains also a tasks chain.

Fig. 8 illustrates the PTAs obtained from Fig. 7 after the translation using Time4sys2imi.

0.A.3 Example with two CPU

Consider again the real-time system modeled in Fig. 1.

Fig. 9 illustrates the PTAs obtained from Fig. 1 after the translation using Time4sys2imi.

0.A.4 Example with 4 CPUs and 11 tasks

We modeled an example with Time4sys presented in Fig. 10. This example contains four CPU and eleven tasks; it also contains four tasks chains.

Fig. 11 illustrates the PTAs obtained from Fig. 10 after the translation using Time4sys2imi

0.A.5 Results