Ning Ge
email: ning.ge@enseeiht.fr

Marc Pantel
email: marc.pantel@enseeiht.fr

Xavier Crégut
email: xavier.cregut@enseeiht.fr

Formal Specification and Verification of Task Time Constraints for Real-Time Systems

Keywords: MDE, RTS, Task, Time Constraint, Formal Specification, Verification, Time Property Patterns, Time Petri Net, Observer-Based Model Checking

Model-Driven Engineering enables to assess a system's model properties since the early phases of its lifecycle and to improve iteratively these models according to the verification results. Safety critical real-time systems have stringent requirements related to the specification and verification of system's task-level time constraints. The common formal methods used to assess these properties for design models rely on a translation of the user models into formal verification languages like Time Petri Net and on the expression of the required properties using Timed LTL (Linear Temporal Logic)/CTL (Computation Tree Logic) or µ-calculus. However, these logics are mainly used to assess safety and liveness properties. Their capability for expressing time related properties is more limited and can lead to combinatorial state space explosion problems during model checking. In addition, they are mainly concerned with symbolic time event-level properties without quantitative time tolerance aspects. This contribution focuses on a formal specification and verification method for system's task-level time constraints (including synchronization, coincidence, exclusion, precedence, sub-occurrence and causality) in both finite and infinite time scope. It proposes a method to translate task time constraints that cannot be assessed by common tools to verifiable time property specifications, which are composed of a set of verifiable time property patterns. These time property patterns are quantitative and independent of both the design modeling language and the verification language as soon as it provides timed elements, making the translation method reusable with different tools. Then, observer-based model checking for Time Petri Nets is used to verify these time property patterns. This contribution analyses the computational complexity and the method's performance for the various patterns. This synchronization properties' specification and verification methods have been integrated in a time property verification framework for UML-MARTE safety critical real-time systems.

Introduction

Model-Driven Engineering enables to verify the system's model properties since the early phases of its lifecycle and to improve iteratively the models according to the verification results. Safety critical real-time systems (RTS) have stringent requirements related to the specification and verification of system's task-level time constraints. However, as the modeling languages commonly used in the industry like UML are only semi-formal, they cannot be directly verified using formal methods. The common approaches used to assess the properties of design models expressed in these languages rely on a translation into a formal verifiable language for both the design model and the assessed properties. However, to our knowledge, two main issues still occur in the state-of-the-art methods.

First, the common verifiable formal expressions used to express the time specifications are Timed LTL (Linear Temporal Logic), CTL (Computation Tree Logic) and µ-calculus. These logics are mainly used to assess safety and liveness properties. Their capability for expressing time related properties is limited and can lead to combinatorial state space explosion problems during model checking.

Second, the common methods are mainly concerned with the logical relations between events, without any quantitative time tolerance whereas RTS requirements usually focus on tasks and more realistic quantitative time, including tolerance. The users may be concerned with the following kind of requirements: Whether Task A and Task B are coincident within the time tolerance 10ms, in each of their occurrences. In such cases, a task is considered as the smallest computable unit in a RTS, which will consume time and modify shared resources (consume and produce). As two simultaneous events cannot be measured without errors in the real world, the concept of time tolerance should be introduced, thus the different clocks should be mapped to the same physical clock. According to these analyses, this contribution provides a task-level specification for the time constraints in RTS and the corresponding verification methods.

This paper focuses on a formal specification and verification method for system's task-level time constraints, in both finite and infinite time scope, for both discrete and dense time. It proposes first a translation from user level time constraints that cannot be verified as such with classical technologies to verifiable time property specifications defined as a set of verifiable time property patterns. These time property patterns are quantitative and independent from both the design modeling language and the verification language as soon as it provides some timed elements, enabling the reuse of this translation. Then, an observer-based model checking method relying on Time Petri Nets (TPN) [START_REF] Merlin | Recoverability of communication protocols-implications of a theoretical study[END_REF] is used to assess that the time property patterns are satisfied. The computational complexity of this proposal is then analyzed. This task-level time constraint's specification and verification method has been integrated in a time properties verification framework for UML-MARTE safety critical RTS [START_REF] Ge | Time properties verification framework for uml-marte safety critical real-time systems[END_REF].

In order to follow the OMG MARTE RTS modeling language, the properties are derived from the same basic semantic elements as CCSL's [START_REF] Peraldi-Frati | Scheduling multi clock real time systems: From requirements to implementation[END_REF] ( coincidence, exclusion, precedence, sub-occurrence, causality) that are extended to cover the requirements for task level specification of quantitative time properties including tolerance. This method provides specification and verification means both for finite and infinite time scope, discrete and continuous time for the task-level time constraints in Table 1. The paper is organized as follows: Section 2 compares our work with related works; Section 3 introduces the methodology; Section 4 introduces a case study; Section 5 presents the specification method for the synchronization properties; Section 7 gives the specifications of time property patterns, illustrates time property patterns verification using observer-based model checking, and discusses the computational complexity and performance to demonstrate the method's applicability; Section 8 gives some concluding remarks and discusses the future works.

Related Works

Several formal specifications of event-level time constraints exist. CCSL (Clock Constraints Specification Language) standardizes clock constraint semantics within UML [START_REF]OMG Unified Modeling Language TM[END_REF] in the MARTE profile to formally express causal and temporal constraints between previously defined symbolic discrete clocks and proposes a process to model time specification. It defines a complete set of clock constraints, which are driven by instantaneous events. However, as it focus on the event-level concept, some adaptation are required for task-level temporal specification and verification. Meanwhile, although it can express the concept of time tolerance, to our knowledge, no the work efficient verification toolset is available for it. Concerning the verification method, CCSL transforms UML model to SyncCharts, and uses Esterel assertions to express clock constraints. This language has a well-defined notion of instant, and at each reaction, any signal has a unique status. This is not the case with non-strictly synchronous languages [START_REF] André | Verification of clock constraints: CCSL Observers in Esterel[END_REF]. It is thus less applicable in for real RTS at detailled design and implementation levels, as the designers must take into account a time duration that must be tolerated by the system.

Methodology

The proposed method is illustrated in Fig. 1. The Transformation of Design Model activity transforms the Design Model to TPN models. Meanwhile, the Transformation of Task Time Constraints activity first translates the Task Time Constraint into Time Constraint Formal Specification, then decomposes the specification into Time Property Patterns. Each time property pattern is quantitative and can be assessed using observer-based model checking. Each time property pattern corresponds to one TPN observer. Then the original TPN and the observer TPN are combined to be model checked by the TINA toolset [START_REF] Berthomieu | The tool tina -construction of abstract state spaces for petri nets and time petri nets[END_REF]. The formal specification method is independent of the design modeling language as soon as it provides timed elements, making it reusable in other verification frameworks. When designing the formal specification and verification methods for tasklevel precedence properties, three temporal aspects should be taken into account:

1. Both logical and physical time concepts. Logical symbolic time can be seen as instantaneous physical time, i.e. physical time with tolerance being zero. 2. Both discrete and dense time domains. Dense time does not introduce any issue in the specification. Problems can occur for the verification technologies. This proposal relies on the TINA toolset for model checking, which supports TPN for a dense time domain. 3. Both finite and infinite time scopes. Time constraint must be assessed for each task occurrence. Finite scope targets events that will happen for a finite number of occurrences in a finite time range, for example aperiodic tasks, while infinite scope concerns those who have infinite occurrence like periodic tasks.

As formal verification is relying on observer-based model checking, it is mandatory to check whether the properties specification approach allows to make the model checking feasible and efficient or not. According to our study so far, for the properties exclusion, sub-occurrence and precedent, the same specification should not be used under the finite and the infinite time scopes as verification gets more complex. Thus, a different specification is applied for finite and infinite time scopes for these properties.

Another important issue is that, although the notion of synchronization should enforce things to occur simultaneously, in the real world, the strict simultaneous character cannot be achieved. This requirement is thus usually associated with a time tolerance. In order to take into account this more realistic fact, this time tolerance is introduced for all the precedence time properties specification. This time tolerance is denoted by δ (δ ∈ R + ).

Case Study

A simple example is used to illustrate the methodology and to evaluate this approach in the following parts of the paper. As the specification method is independent of the modeling languages, no specific diagram is used for any of them.

A classical asynchronous RTS model is provided in Fig. 2. According to the general asynchronous message-driven pattern, the Sender will regularly distribute data to the two receivers Calculator A and Calculator B through the Router. The receivers provide redundant control service. They will do some computation after receiving the data. The redundant controller requires that the output of the two calculators must be available at the same time in each working cycle; otherwise, the servo of the corresponding actuator cannot correctly unify the redundant command. In this case, the designer need to verify the coincidence of computation tasks between calculators A and B. As it is impossible to respect a strict simultaneous timing with an explicit local synchronisation, a time tolerance is defined. Once the two time instants fall into the same time window (size of window equals to tolerance), they are considered as coincident.

Formal Specification of Task Time Constraint

In this section, some preliminary definitions are given to help understand the formal specification, then the formal specification is illustrated for the coincidence time constraint used in the case study. Due to page limits, the formal specifications for the other time constraints are given without detailed explanations.

Preliminary definitions

Definition 1 (Task). In the system, a task is considered as the smallest computable unit, which consumes time and modifies resources (consumes and produces). It computes the outputs using the inputs. A task could be executed infinitely or finitely according to the design. Definition 2 (Presence). The presence of a task is the time duration [t s , t e ] of task's execution, where t s and and t e are the start and end time instant. Definition 3 (Occurrence). Occurrence is an instant concept. It is used to precise the occurrence of the associated inner event (start and end).

To simplify the presentation, some symbols are defined in Table 2.

Formal Specification of Coincidence Time Constraint

Coincidence Task X and Y are coincident if f. the n th occurrence of X occurs simultaneously with the n th occurrence of Y while n ∈ N. It is equivalent saying the n th occurrence of X s (e) occurs simultaneously with the n th occurrence of Y s (e). In Fig. 3(a), the X and Y are coincident.

Specification 1 (Coincidence -Infinite Time Scope) C if t (X, Y, δ) ≡ ∀t ∈ R + : (|O(X t s ) -O(Y t s )| < 2) ∧ (|O(X t e ) -O(Y t e )| < 2) (1)
X[i] X[i+1] Y[i] Y[i+1] Coincidence(X,Y, ) = true X Y X[i] X[i+1] Interleave Coincidence(X,Y, ) = false Y[i] Y[i+1] (a) (b) Figure 3. Coincidence ∀t ∈ R + : (|T (X t s ) -T (Y t s )| < δ) ∧ (|T (X t e ) -T (Y t e )| < δ) (2) ∀i ∈ N * : (T (X i e ) + δ < T (Y i+1 s )) ∧ (T (Y i e ) + δ < T (X i+1 s )) (3)
Specification 2 (Coincidence -Finite Time Scope)

C f t (X, Y, δ) ≡ (O(X s ) = O(Y s )) ∧ (O(X e ) = O(Y e )) (4) ∀i ∈ [1, O(X s )] : (|T (X i s ) -T (Y i s )| < δ) ∧ (|T (X i e ) -T (Y i e )| < δ) (5) ∀i ∈ [1, O(X e ) -1] : (T (X i e ) + δ < T (Y i+1 s )) ∧ (T (Y i e ) + δ < T (X i+1 s )) (6)
In formula (1) of infinite time scope, at time t, the occurrence difference between X s(e) and Y s(e) should be inferior to 2; in formula (4) of finite time scope, the occurrence times of X s(e) should be equal to that of Y s(e) . In formulas ( 2) and ( 5), the i th occurrence of X s(e) occurs simultaneously with the j th occurrence of Y s(e) , within time tolerance δ. i = X t s , j = Y t s , as defined in Table 2. In formula (3) and ( 6), with the time tolerance introduced, it is possible that an interleave exists between i th occurrence of X and (i + 1) th occurrence of Y , which violates the coincidence definition. So constraints for consequent occurrences must be added. In Fig. 3(b), the model satisfies formulas (1) (4) and (2) (5), but violates the formulas (3) (6). The two tasks are not coincident.

Formal Specification of other Task Time Constraints

Synchronization Logical synchronization is a reduced coincidence relation without restricting a simultaneously execution. The only concern is that the execution order must persist.

Specification 3 (Synchronization -Finite Time Scope) Syn f t (X, Y, δ) ≡ (O(X s ) = O(Y s )) ∧ (O(X e ) = O(Y e )) ∀i ∈ [1, O(X e ) -1] : (T (X i e ) + δ < T (Y i+1 s )) ∧ (T (X i e ) + δ < T (X i+1 s )) Specification 4 (Synchronization -Infinite Time Scope) Syn if t (X, Y, δ) ≡ ∀t ∈ R + : (|O(X t s ) -O(Y t s )| < 2) ∧ (|O(X t e ) -O(Y t e )| < 2) ∀i ∈ N * : (T (X i e ) + δ < T (Y i+1 s )) ∧ (T (Y i e ) + δ < T (X i+1 s ))
Exclusion Task X and Y are in excluded, if f. Not any presence of X occurs simultaneously with any presence of Y . It could be considered as another form of coincidence with some time offset. For this reason, it also needs the constraint for interleave problem. The schema of exclusion is shown in Fig. 4.

X[i] X[i+1] Y[j] Y[j+1] Exclude(X,Y, ) = true X[i] X[i+1] Y[j+1] Exclude(X,Y, ) = false Y[j]
E f t (X, Y, δ) ≡ ∀i ∈ [1, O(X s )], ∀j ∈ [1, O(Y s )] : T (X i s ) + δ < T (Y j s ) ⇒ (T (X i e ) + δ < T (Y j s )) ∧ (T (Y j e ) + δ < T (X i+1 s )) T (X i e ) + δ < T (Y j s ) ⇒ T (Y j e ) + δ < T (X i+1 s ) T (X i s ) + δ < T (Y j e ) ⇒ T (X i e ) + δ < T (Y j s ) T (X i e ) + δ < T (Y j e ) ⇒ (T (X i e ) + δ < T (Y j s )) ∧ (T (Y j e ) + δ < T (X i+1 s ))
As the finite time semantics are not computable in infinite time scope. Some constraints are required to ensure that between two continuous occurrences of task X, it exists and only exists one occurrence of task Y, and vice versa.

Specification 6 (Exclusion -Infinite Time Scope)

E if t (X, Y, δ) ≡ ∀t ∈ R + : (|O(X t s ) -O(Y t s )| < 2) ∧ (|O(X t e ) -O(Y t e )| < 2) ∀i ∈ N * : T (X i s ) + δ < T (Y i s ) ⇒ (T (X i e ) + δ < T (Y i s )) ∧ (T (Y i e ) + δ < T (X i+1 s )) T (X i e ) + δ < T (Y i s ) ⇒ T (Y i e ) + δ < T (X i+1 s ) T (X i s ) + δ < T (Y i e ) ⇒ T (X i e ) + δ < T (Y i s ) T (X i e ) + δ < T (Y i e ) ⇒ (T (X i e ) + δ < T (Y i s )) ∧ (T (Y i e ) + δ < T (X i+1 s ))
Sub-occurrence Task Y is a sub-occurrence of task X, if f. The i th occurrence of X and the j th occurrence of Y occur simultaneously, where always j i. The schema of sub-occurrence is shown in Fig. 5.

Specification 7 (Sub-occurrence -Finite Time Scope)

S f t (X, Y, δ) ≡ (O(X s ) O(Y s )) ∧ (O(X e ) O(Y e )) ∀j ∈ [1, O(Y s )], ∃i ∈ [j, O(X s )] : (|T (X i s ) -T (Y j s )| < δ) ∧ (|T (X i e ) -T (Y j e )| < δ) ∧ (T (X i-1 e ) + δ < T (Y j s )) ∧ (T (Y j e ) + δ < T (X i+1 s ))
The computable semantics for infinite time scope constraints the semantics. The faster one's occurrence is always k(k ∈ N * ) times multiple of the slower one's.

X[i] Sub-Occurrence(X,Y, ) = true Sub-Occurrence(X,Y, ) = false X[i+1] X[i+2] Y[j] Y[j+1] X[i] X[i+1] X[i+2] Y[j] Y[j+1] Interleave Figure 5. Suboccurrence Specification 8 (Sub-occurrence -Infinite Time Scope) S if t (X, Y, δ, k) ≡ ∀t ∈ R + : (|O(X t s )/k -O(Y t s )| < 2) ∧ (|O(X t e )/k -O(Y t e )| < 2) ∀i ∈ N * : (|T (X i•k s ) -T (Y i s )| < δ) ∧ (|T (X i•k e ) -T (Y i e )| < δ) ∧ (T (X i•k e ) + δ < T (Y i+1 s )) ∧ (T (Y i e ) + δ < T (X i•k+1 s ))
Precedence Task X precedes task Y if f. At any time, the occurrence of X is more than or equal to the occurrence of Y . This implies X i s must precede Y i s , however it is not necessary to also have X i e precedes Y i s in all context. So to clarify the strict level of specification, L 1 (less strict), L 2 (strict), L 3 (very strict).

Specification 9 (Precedence -Finite Time Scope)

P f t (X, Y, δ, L 1 ) ≡ ∀i ∈ [1, O(X s )] : T (X i s ) + δ < T (Y i s ) P f t (X, Y, δ, L 2 ) ≡ ∀i ∈ [1, O(X s )] : (T (X i s ) + δ < T (Y i s )) ∧ (T (X i e ) + δ < T (Y i e )) P f t (X, Y, δ, L 3 ) ≡ ∀i ∈ [1, O(X s )] : T (X i e ) + δ < T (Y i s )
The computable specifications for infinite time scope constrains the semantics, and it is the same as the causality definition in infinite time scope.

Causality Causality is similar to Precedence, except that it requires the maximum possible occurrence of X equals to that of Y , because each occurrence/execution of X causes the corresponding occurrence of Y .

Specification 10 (Causality -Finite Time Scope)

C f t (X, Y, δ, L 1 ) ≡ O(X) = O(Y ), P f t (X, Y, δ, L 1 ) C f t (X, Y, δ, L 2 ) ≡ O(X) = O(Y ), P f t (X, Y, δ, L 2 ) C f t (X, Y, δ, L 3 ) ≡ O(X) = O(Y ), P f t (X, Y, δ, L 3 ) Specification 11 (Causality -Infinite Time Scope) C if t (X, Y, δ, L 1 ) ≡ ∀t ∈ R + : (|O(X t s ) -O(Y t s )| < 2) ∧ (|O(X t e ) -O(Y t e )| < 2) ∀i ∈ N * : T (X i s ) + δ < T (Y i s ) C if t (X, Y, δ, L 2 ) ≡ ∀t ∈ R + : (|O(X t s ) -O(Y t s )| < 2) ∧ (|O(X t e ) -O(Y t e )| < 2) ∀i ∈ N * : (T (X i s ) + δ < T (Y i s )) ∧ (T (X i e ) + δ < T (Y i e )) C if t (X, Y, δ, L 3 ) ≡ ∀t ∈ R + : (|O(X t s ) -O(Y t s )| < 2) ∧ (|O(X t e ) -O(Y t e )| < 2) ∀i ∈ N * : T (X i e ) + δ < T (Y i s )
6 Time Property Patterns

All the above specifications can be expressed by a set of time property patterns, in finite time scope and in infinite time scope. For example, in section 5.2, formula (2) contains the time property pattern Max interval between two events. All the time property patterns used in the formal specification of task time constraints are listed in Table 3 and Table 4.

i E i/k Occurrence difference ∀t ∈ R+, k ∈ N * : |O(X t s )/k -O(Y t s )| < δ Minimum time interval between events E1 and E2 ∀i ∈ N * , k ∈ N * , b ∈ N, j = i • k + b : |T (E i 1 ) -T (E j 2 )| > δ Maximum time interval between events E1 and E2 ∀i ∈ N * , k ∈ N * , b ∈ N, j = i • k + b : |T (E i 1 ) -T (E j 2 )| < δ
In the case study, there are 4 time property patterns (Table 5) for the coincidence time constraint in infinite time scope. To assess the coincidence time constraint, the method will compute the values of these 4 quantitative property patterns.

The verification method will be introduced in the next section. To assess the time property patterns by model checking, the common formal methods used rely on a translation of the user models into a formal verifiable language and express the required properties using verifiable formal expressions. TPN is selected as the verification model in this work, because it allows expressing and verifying time properties under both logical and chronometric time models. Fig. 6 is a TPN example. Compared to Petri Nets, the transitions in TPN are extended with a time constraint that controls the firing time. For example, transition T 1 is attached with time constraint [19,27]. When the token arrives at place P 1 , the local of T 1 starts. Between 19 and 27 time units, T 1 can be fired.

For the verification of one time property pattern, an observer TPN structure is added into the original TPN, and then TINA is used to verify the observerdedicated LTL/CTL/Marking formulas on the combined TPN. As model checking significantly consumes time and memory resource, we use the following 2 approaches to ensure the verification performance.

-When doing the model checking, the TPN shall perform the highest possible abstraction to unfold the reachability graph. This high abstraction model should preserve the desired time property. The model-checking is on-the-fly. -Each formula's verification is independent in terms of reachability graph generation, so a parallel computation is possible.

Verification of Time Property Pattern

|T (a t ) -T (b t )| < δ
One of the property patterns, |T (a t )-T (b t )| < δ, has been chosen to illustrate the verification method. For the page limits, the other observers will be presented in another paper or technical report. The principle for deciding whether two events are always occurring in a given bound is to find out whether one could advance the other by time δ. An observer pattern (Fig. 7) is added to the original TPN. The middle transition will always instantly neutralize the tokens from the places Occ A and Occ B except when one token waits for a time longer than δ that leads to the firing Once it is known how to verify |T (a t ) -T (b t )| < δ, it is possible to change δ to compute a near optimal tolerance. If |T (a t ) -T (b t )| < δ + 1 is verified as true, but false for |T (a t ) -T (b t )| < δ, then the near optimal tolerance is δ + 1. In order to improve the computation efficiency, a dichotomy search is used to reduce the complexity from O(N ) to O(log N ) using divide and multiply by two instead of add or subtract one.

Computational Complexity Analysis

Coincidence time constraint is taken as example to analyse the computational complexity. As the observers for infinite and finite time scope are different, the two cases are respectively analyzed. For simplicity of the presentation, one Kripke Transition Systems (KTZ) generation time is taken as the unit of time (ut).

In the infinite time scope, as shown in Table 5 and Specification 1, its formal specification contains 4 time property patterns: Representation of the next occurrence of event, Occurrence difference between events X t a and Y t a , Maximum time interval between events X t a and Y t a , and Minimum time interval between events X t a and Y t b . For formula (1), it will respectively calculate the value for

|O(X t s ) -O(Y t s )| < 2 and |O(X t e ) -O(Y t e )| < 2.
Each of them corresponds to one KTZ generation for the TPN with observer. Thus, the computational complexity for formula (1) is 2(ut). Likewise, the computational complexity for formulas (2) and (3) are both 2(ut). The computational complexity of coincidence in infinite time scope is 6(ut). Thus, in the infinite time scope, the computational complexity is a constant, which means it is independent of the system's design.

In the finite time scope, as shown in Specification 2, it also contains 3 property patterns. In formula (4) (O(X s ) = O(Y s )) ∧ (O(X e ) = O(Y e )), it will calculate the occurrence's upper bound of start event and end event. The upper bound of event's occurrence is denoted A. As a dichotomy search is used to reduce the complexity, the computational complexity of O(X s or O(X e ) is A • log 2 A, denoted as B. Thus, the computational complexity of formula (1) is 2B(ut). In formula [START_REF]OMG Unified Modeling Language TM[END_REF]

, to calculate |T (X i s ) -T (Y i s < δ, is in fact to calculate respectively T (X i s ) -T (Y i s ) < δ and T (Y i s ) -T (X i s ) < δ.
For each of them the complexity is A(ut), because it should calculate the times of the upper bound of the event's occurrence. Thus, the complexity of formula ( 5) is 4A(ut), and of formula ( 6) is 2A(ut). The whole computational complexity of coincidence in finite time scope is 6A+2B. Thus, in the finite time scope, the computational complexity depends on the complexity of system's design.

The computational complexity of all the mentioned time constraints are listed in Table 6, for both finite and infinite time scope. These numbers allow to conclude that the verification method guarantees a low computational complexity.

Performance Analysis

In TPN model checking, the computational performance depends on both the cost of generating the KTZ and the cost of assessing the formulas for the KTZ. The former produces the major cost, while the later produces the minor cost once the decidability has been proved. The computational performance is analyzed for the time property patterns, then the computational performance of the task time constraints can be deduced using the complexity table, Table 6.

As the performance depends on the system's scale, it is important to measure the performance influence produced by the observer TPN added into the original TPN. Both the performance of the original TPN and of the observeradded TPN are evaluated. This influence is computed by comparing the KTZ generation cost of the original TPN and that of the observer-added TPN. In order to make this performance result demonstrate that the method is applicable for pragmatic systems, the systems are randomly generated scaling from 2 to 10 parallel threads, where each thread disposes of 10 to 100 periodic tasks. As shown in Fig. 8, the influence for pattern Occurrence Difference is controlled in 15%; for pattern Maximum Time Interval, it is controlled in 40%; and for pattern Minimum Time Interval is also controlled in 40%. The influence test result demonstrates that the over-cost of the observer is very slight, thus, the observer-based model checking method's performance is very stable. If the original TPN can terminate its KTZ generation in an acceptable time range,the cost of time constraint's verification is also acceptable. This demonstration is for the infinite time scope property patterns. The same approach allows to demonstrate the performance for the property patterns in finite time scope, the results are given in Fig. 9. For the page limits, the analysis is not detailled.

Conclusion

The common system time constraint specification and verification methods focus on the symbolic event-level and have not considered the quantitative time with tolerance.

This paper focuses on the formal specification and verification methods for system's task-level time precedences properties (including synchronization, coincidence, exclusion, precedence, sub-occurrence, causality) in both finite and infinite time scope. It proposes first a method to translate the non-verifiable time constraint to verifiable time property specifications, which are composed of a set of verifiable time property patterns. The time property patterns are quantitative and independent of both the design modeling language and the verification language if they provide timed elements, making the translation method reusable. Then, an observer-based model checking method using Time Petri Nets is used to assess the time property patterns. The computational complexity and the method's performance are analyzed. This synchronization properties' specification and verification method has been integrated in a time properties verification framework for UML-MARTE safety critical real-time systems.

In the future, on the technical side, we will optimize the TPN by finding some reducible structural patterns without influencing the system. On the application side, we will apply this approach in the industrial applications, and integrate this reusable approach into other time properties verification dedicated frameworks.

Figure 2 .

 2 Figure 2. Case Study System Model

Figure 4 .

 4 Figure 4. Exclusion Specification 5 (Exclusion -Finite Time Scope)E f t (X, Y, δ) ≡ ∀i ∈ [1, O(X s )], ∀j ∈ [1, O(Y s )] : T (X i s ) + δ < T (Y j s ) ⇒ (T (X i e ) + δ < T (Y j s )) ∧ (T (Y j e ) + δ < T (X i+1 s )) T (X i e ) + δ < T (Y j s ) ⇒ T (Y j e ) + δ < T (X i+1 s ) T (X i s ) + δ < T (Y j e ) ⇒ T (X i e ) + δ < T (Y j s ) T (X i e ) + δ < T (Y j e ) ⇒ (T (X i e ) + δ < T (Y j s )) ∧ (T (Y j e ) + δ < T (X i+1 s ))

Figure 6 .

 6 Figure 6. Time Petri Net Example

Figure 7 .

 7 Figure 7. |T (A t ) -T (b t )| < δ Pattern TPN Observer

Figure 8 .

 8 Figure 8. Performance Influence of the Observer-Based Model Checking Method

Figure 9 .

 9 Figure 9. Performance Influence of the Observer-Based Model Checking Method

Table 1 .

 1 Task-level Time Constraints

	Definition	Task-level Time Constraints
	Coincidence	Two task executions are coincident
	Synchronization	Synchronization of two tasks
	Exclusion	Mutual exclusion of two tasks' execution
	Sub-occurrence One task is another one's sub-occurrence
	Precedence	One task is preceding another
	Causality	One task is causal with respect to another

Table 2 .

 2 Symbols for Formal Specification

	Symbol Definition
	X	Task X
	X i The i th presence of task X
	Xa The inner event 1 a of task X
	X i a	The i th occurrence of Xa
	X t a	The occurrence of Xa which is the nearest
		(forward or backward) to the time instant t
	T (X i a ) The occurring time instant of X i

a T (X t a ) The occurring time instant of X t a O(X) The maximum possible presence of task X. O(Xa) The maximum possible occurrence for Xa. O(X t a ) The occurrence count for Xa at time t

Table 3 .

 3 Finite Time Scope Time Property Patterns Min time interval between events Ei and Ej ∀i, j ∈ N Max time interval between events Ei and Ej ∀i, j ∈ N

	Time Property Pattern	Formal Specification
	Max Occurrence Count	∀i ∈ N

* : O(X i s ) < constant * : T (E i 1 ) -T (E j 2 ) > δ * : T (E i 1 ) -T (E j 2 ) < δ

Table 4 .

 4 Infinite Time Scope Time Property Patterns Time Property PatternsFormal Specification Representation of the next k th occurrence of event E i E i+k Representation of the (i/k) th occurrence of event E

Table 5 .

 5 Time Property Patterns

	Formal Specification	Time Property Pattern
	X i+1 s		Representation of the next occurrence of event X i s
	|O(X t a ) -O(Y t a )| < δ Occurrence difference between events X t a and Y t a
	|T (X t a ) -T (Y t a )| < δ	Max time interval between events X t a and Y t a
	T (X i e ) + δ < T (Y i+1 s	)	Min time interval between events X t a and Y t b

Table 6 .

 6 Computational Complexity of Task Time Constraints

	Task Time Constraint Finite Time Infinite Time
	Coincidence	6A + 2B	6
	Synchronization	2A + 4B	4
	Exclusion	6A 2	8
	Sub-occurrence	7A 2 + 2B	6
	Precedence (less strict)	A	3
	Precedence (strict)	2A	4
	Precedence (very strict)	A	3
	Causality (less strict)	A + 2B	3
	Causality (strict)	2A + 2B	4
	Causality (very strict)	A + 2B	3

The inner events in this paper could be the start of task (Xs) or the end of task (Xe).

This work was funded by the French ministries of Industry and Research and the Midi-Pyrénées regional authorities through the ITEA2 OPEES and FUI Projet P projects