- Timed automata with durational actions (daTA) are a form of timed automata that admit a more natural representation of durational actions and capturing true concurrency, with those additional benefits the kinds of properties to be verified on real-time systems will be enlarged. We present a novel approach to construct a region graph, based on the maximality semantics and preserving that specificity. More precisely, we renew the maximality capabilities on the region graph; we propose the MRG construction algorithm. We also describe an implementation of this construction (TaMaRG tool). The approach is illustrated by means a case study.
Riadh MATMAT
Ilham KITOUNI
Souad GUELLATI
D-Eddine SAIDOUNI, 1. INTRODUCTION Nowadays, formal verification becomes increasingly used in the industry as a part of the design process. There is a growing need for efficient tools dealing with real aspects of systems.
Model Checking [
In general, the system is firstly described using a
high level specification models (as timed Petri
net [
Timed Automata (TA) [
In spite of this, the model suffers from many problems (decidability, state space explosion...) which is impeding its scalability.
Many studies have pointed the interest of TA, its
underlying semantic is said the interleaving
semantics [
Decidability proof of the reachability problem in
TA model is based on a finite abstraction of the
set of the clock valuations. The result of this
abstraction is the region graph [
It’s obvious that in real world systems, actions are not instantaneous and have durations. This realistic characteristic is important in many cases.
Instead of the interleaving semantics, maximality
semantics has been proved necessary and
sufficient for carrying both the refinement
process and action durations [
Durational actions timed automata model (daTA) was proposed as a timed automata coated by the maximality semantics. daTA model allows to carry durations of actions and to handle true concurrency; which are realistic assumptions for specifying timed systems.
Indeed, to model duration of actions, every edge of the automaton is annotated by constraints on clocks. Implicitly constraints on the edges contain the durations of actions, those that are already started. In addition, other real-time aspects are considered (like delaying the start and deadlines). A single clock is reset on every edge; it corresponds to the beginning of event (action). The termination of an action will be captured by information on locations of the automaton, precisely on the destination location of transition. In reality, the action duration is represented by both in the constraints (guards) of the following edges and on the next locations and that means action is not over yet. To better understand these principles, consider two actions, if their executions are dependent, then one should expect the termination of the other, this will be realized by the use of the duration of the first action in the guard of the second one. Otherwise they are in concurrency (parallel executions). See the example depicted Figure 1.
Another important aspect of real-time systems is
the urgency (i.e., actions whose execution
cannot be delayed beyond a certain time bound).
In daTA model urgency is represented by
deadlines as proposed in [
Unfortunately, the region graph of TA doesn’t contain information about durations or parallel execution of actions; those limitations motivate the development of Maximality based Region Graph (MRG) from durational action timed automata.
Our contribution: In order to preserve all achievements of the maximality semantics namely duration of actions and true concurrency, we will use the data model and information concerned by the maximality when developing the region graph. We are interested by the preservation of the maximality semantics even on the abstracted graph of executions of daTA. The fundamental interest of this approach is to propose a structure based on classical regions for model checking and all other validation requirements of concurrent real-time systems (possibly distributed).In this paper we expand a theory of region abstraction to capture novel aspects which are relevant for verifying true concurrency and resulting from the maximality semantics.
In fact for the model checking based on daTA
model, the range of proprieties to be verified is
enlarged to capture actions incompatibility, auto
concurrency and the concurrency degree
specification [
For this purpose we propose an algorithm for generating Maximality-based Region Graph (MRG). We also describe an implementation of this algorithm, which allows the construction of the MRG and its transformation into dotty grammar. Finally, the tool is experimented by means a case study in order to illustrate its functionalities and to show its capabilities to deal with real systems.
Paper Outline: duration actions timed automata are recalled in Section 2. Definition and formalization of Maximality based Region Graph are proposed in Section 3. Section 4 presents the construction algorithm of MRG with an illustrative example. Section 5 describes the associated tool (TaMaRG) and the major functionalities. Also, a case study is presented and results are commented in this section, namely sender parts of alternative bit protocol. Section 6 concludes the paper and gives some perspectives on future work. 2. TIMED AUTOMATA WITH DURATION
OF ACTIONS
2.1. daTA model
The daTA model (durational actions timed
automata) [
Illustrate this model by an example (Figure 1): {∅} , ≔ S0 ≤ { ≥ } , ≔
S1 ≤ ≤ { ≥ }
S2 The duration associated to the action is represented by constraints on the transitions and in the target states of each one. In this sense, any enabled transition represents the beginning of the action execution. On the target state of transition, a timed expression means that the action is possibly under execution. From operational point of view, each clock is associated to an action. This clock is reset to 0 at the start of the action and will be used in the construction of the temporal constraints as guard of the transitions.
Fig.1 presents a system of two consecutives actions and , the clock is associated to the action , on the locality the temporal formula { ≥ 1} represents the duration of the action (which is important to distinguish from invariant in timed automata).
The end of an action execution is deduced implicitly in the case of an action that it is causally dependent. The action depends on , so the transition is guarded by constraint formed by duration of and more time {1 ≤ ≤ 2}. Starting from this, we can express different possibilities of real time systems behaviour like delaying execution of action or limiting its offering time by manipulation clocks constraints. Consider another example depicted by Figure 2; the system consists of two concurrent processes 1 and 2 synchronizing on an action . The process 1 executes the action followed by , while 2 executes then , and suppose that actions , and have respectively 10, 12 and 4 units of time as durations.
In daTA of Fig.2, from the state , the actions and can comply in parallel, and each one can finish only if its clock reaches a value equal to its duration, from where duration condition set { ≥ 10, ≥ 12} .
≥ 12 . Once this latter is satisfied, can start at any time in the enabling open interval ∈ [10,+ ∞ [, ∈ [12,+ ∞ [, the so called enabling domain.
Another concept of real time systems is urgency
in our proposal it’s represented as deadlines
[
guarantees that if time cannot progress, at some state at least one action is enabled from this state. 2.2. Formalization
numbers. A clock takes values from ℝ . Given a set ℋ of clocks, a clock valuation over ℋ is a function assigning a non negative real number to every clock. The set of valuations of ℋ noted
valuation is a mapping on ℋ to ℝ . Let be a clock, the valuation [ ← 0] resets clock to 0 and each other clock to ( ) . The valuation + maps every clock to ( ) + , ∈ ℝ .
following grammar: ∷= | | ~ | ∧ , where ∈ ℋ , ∈ ℕ and ~ ∈ {< ,> ,≤ ,≥ }. The satisfaction with respect to clock valuation function written ⊨ means that according the valuation function , evaluates to true.
constraints, ranged over by and also by . We also use a subset of constraints where only the atomic form of clocks comparison is allowed.
∷= ≥ , where ∈ ℋ and ∈ ℕ . This subset represents condition duration over a finite set of actions noted . Definition2.1. A daTA is a tuple = ( , ,ℋ , , ) over , where is a finite set of states, ∈ is the initial state, ℋ is a finite set of variables named clocks. ⊆ × (ℋ )× (ℋ )× × ℋ × is a finite set of transitions.
Given a transition = ( , , , , , ′) ∈ , represents an edge from location to ’ that launch the execution of action a whenever guard becomes true. In addition, deadline imposes an urgency condition: the transition cannot be delayed whenever is satisfied, is a clock to be reset at this transition.
which decorates each state by a set of timed formula named action durations; these actions are potentially in execution on it. ( ) = ∅ means that no action is yet started.
We define Clock Label Occurrence : (ℋ ) → 2ℋ , as a function which gives clock names occurred in a given timed formulas, recursively by: ⎧ ⎪ ( ) = ( ({ ~ }) = { } ) = ∅ ⎨ ( ∧ ∧ … ∧ ) = ( ) ⎪ ⎩ ..
Such as:
∈ (ℋ ), ∈ ℋ ,∼∈ {< ,> ,≤ ,≥ }and ∈ ℕ . It is a function which gives clock names occurred in a given timed formulas.
Definition2.2. The semantics of a daTA A is a timed transition system = ( , ,→) over ∪ ℝ . A state of (or configuration) is a pair (s,v)such as s is a state of A and v is a valuation over ℋ , where: = {( , ) | ∈ ∈ ℋ }; = ( , ) such that ∀ ∈ ℋ , ( ) = 0 ; → ⊆ × ( ∪ ℝ ) × consist of the discrete and continuous transitions.
,,,,, ∈ 1 = ⊨ .
( ,) ⎯⎯ ( , [ ≔ ]) The continuous transition is defined for all ∈ ∈ℝ ∀ , ⊨ ( ) , where ℝ by 2 =
( , ) ⎯⎯ ( , )
( ) = ¬⋁( |∃ ∈ : = ( , , , , , ′)) is
the time progress condition in [
REGION GRAPH Characterization of equivalent behavior using the temporal maximality semantics and verification by enumeration (model-checking) must pass through abstractions of durational actions timed automata, that both: Generate a finite graph (finite system transitions); Preserve the degree of parallelism; Preserve the system properties.
Several verification problems such as
reachability analysis, untimed language
inclusion, language emptiness as well as timed
bisimulation can be solved by techniques based
on the region abstraction [
( ) denotes the fractional part of , and ⌊ ( ) ⌋ denotes the integral part of .
Definition3.1. Let = ( , , ,ℋ , ) be a daTA.
that ( ≤ ) or ≤ is a sub-formula of some clock constraint appearing in .
The equivalence relation ≅ is defined over the set of all clock interpretations for ℋ ; v ≅ v′ iff all the following conditions hold: i. For all ∈ ℋ , either ⌊ ( ) ⌋ and ⌊ ′( ) ⌋ are the same, or both ( ) and ( ) are greater than . ii. For all , ∈ ℋ ( ) ≤ and ( ) iff ′ ( ) ≤ iii. For all ∈ ℋ ( ) ≤ , ( ) = 0 iff ′ ( ) = 0 .
The equivalence relation ≅ is defined over the set of all clock interpretations for ℋ . We will use [ ] to denote the equivalence classes of V(ℋ ) to with ( ) ≤ ( ) ≤ ′ ( ) .
with which
belongs. It also clock regions denoted by: = [ ] = { ′ ∈ (ℋ )| ≅ ′} .
Example 3.1. Consider a daTA and with = 2 and = 1.
with two clocks 1 0 1
2 The clock regions shown in Figure 3 are: 14 open line segments: e.g. [0 < = < 1]; 8 open regions: e.g.[0 < < < 1] ; 6 corner points: e.g. [ = 1, = 1] . We call end-region the region satisfying the following condition: ∀ , ∈ ℋ ⇒ > . The end region is open to infinity on all clocks region. It does not have a successor region, in Figure 3 the end-region is [x > 2, > 1]. 3.2. Successor function Let and ′ be regions. The region ′ is a successor of , noted ( ) = ′ iff ∀ ∈ ⇒ ∃ ∈ ℝ and + ∈ ′.
Now we are ready to define the Maximalitybased Region Graph associated to a daTA = ( , , ,ℋ , ) . 3.3. Regions Graph Coated of Maximality
Graph of a daTA A. Similar to region automaton
[
According to the maximality semantics and the daTA structure, each state of Maximality-based Region Graph contains a set of clocks which corresponds to events for actions under executions. Those events are captured by timed formulas initially on states of daTA (delivery by function). The function ( , ) presented in definition 3.2 ensures this feature.
The transitions relation of ( ) is an extension of transitions relation defined for a region automaton. It has an edge from ( , ) to ( ′, ′), labeled with ( ), , , where is a clock associate to the action and ( ) the set of clock names corresponding to the actions conditioning the execution of . This is effective if in daTA a transition of the form ( , , , , , ) ∈ . As usual the transitions relation can be defined using a successor function over the clock regions and some maximality functions.
Definition3.2. Let = ( , , ,ℋ , ) be a daTA. The Maximality-based Region Graph associated to A is ( ) = , 0, , where: ii. iii.
, is a set of states regions having the form ( , ) with ∈ and is a region.
= ( , ), is the initial state region, where s is the initial state for and = [ ( )]such as ∀ ∈ ℋ , ( ) = 0.
∶ × → 2 ℋ , is a maximality function assigning to each state region ( , ) a finite set of clocks representing maximal event names. It’s defined as: ( , ) = { | ≥ ∈ ( )}. iv. The transition relation is defined by two kinds of transitions: Passage of time. Each region ( , ) , where is not an end class, has an edge to its successor ( , ( )). Formally we write: ⊨ ( ) ∧ ( ) ⊨ ( )
( , ) ( , ( )) Transition of . Given a region ( , ) , for each transition = ( , , , , , ′ ) ∈ , there is an edge to ( , ′) where: = [ ≔ 0 ], ⊨ and ⊨ ( ′) .
This is formalized by the rule: ,,, ⎯⎯⎯ [ ≔ 0 ] ⊨ ( ′) ∧ ⊨ ∧
( ),, ( , ) ⎯⎯⎯⎯⎯⎯⎯⎯ ( , [ ≔ 0 ]) 4. Generating Maximality-based Region
Graph In this section we propose an algorithm which constructs the Maximality-based Region Graph for durational actions timed automata. It is based on the successor function and maximality semantics to create new regions by using the daTA structure. Output :Maximal-based Region Graph corresponding Ato be the initial
state region of MRG ; calculate
for each clock ∈ ℋ . let (P ←, ∅); enqueue (P; l ); // = ( , ) while P not emptydo = dequeue( ); // = ( , ) if is not end regionthen
Switch type_region( ) if ⊨ case type_1: ’ = case type_2 :’ = case type_3 :’ =
( ) ∧ = ( , ) add ′ to ; add
to ; ∶ → ′ ; enqueue ( ; ′); ( ′) ≔ { | ≥ ∈
( )} ( , ( , ( , _1); _2); _3); ( ) ⊨ ( ) then end if add to ;
( ), , : ⎯⎯⎯⎯⎯⎯⎯⎯ add to
; enqueue ( ; ); ∈ ; ( )} The Algorithm: Initially the daTA is traversed so as to find for each clock ∈ ℋ . This is required for abstraction and ensuring finite number of states regions in the MRG. After creating initial state region of MRG, the algorithm calculates the successor regions. Regions are specified by one of three forms (type_1, type_2, type_3).
The function returns a successor of current region. In this step the algorithm checking under the successor region guard and TPC of daTA for creating regions states and transitions, the regions states are creating with keeping all actions under execution, this is performed by the function , the transitions are created either by passage of time(delay transitions) or by actions (discrete transitions).
Delay transition is created if the current region and its successor satisfies the TPC, while discrete transitions is created if the region satisfies the guard and satisfies the TPC, in this case, we keep (on the transition) clock associated with the action and clocks corresponding to actions under execution. Recall that those actions condition the launching of current transition. This is performed by the function .
constructed, to capture the maximal events and to ensure maximum information on concurrency. The MRG generated by this algorithm correspond to daTA of Figure 1, is represented by Figure 4. 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14 15: 16: 17: 18: 19: 20: 21: 22: 23 24: 25: 26: 27: 5. Implementation and case studies 5.1. Implementation TaMaRG is a tool for generating Maximalitybased Region Graph from durational actions timed automata. This tool has a graphical editor to draw and edit daTA structure Figure 6. The MRG-generator generates a maximality-based region graph, and MRG-Dotty adaptor produces a dot file type as showed in Figure 7. Its functional view is sketched in Figure 5. The input is a daTA of the intended behavior of the system under verification, the output is an MRG.
The entire tool was implemented using java as programming language.
5.2. Case studie
ABP Protocol: ABP (Alternating Bit Protocol) is
a connection-less protocol for transferring
messages in one direction between a pair of
protocol entities. It is a simple form of the Sliding
Window Protocol with a window size of 1 [
The aim of this section is to illustrate the use of daTA tool; we will focus on sender part. The Model: The alternating bit protocol consists of a sender S, a receiver R, a channel K from S to R and a channel L from R to S, its architecture is as follow: The sender S and receiver R communicate via the same lossy communications mediums (L and K). So messages may be lost. The basic principle is to stamp messages with a one bit sequence number. When a protocol entity sends message (either Data or Acknowledgment) with sequence number b. The next message it receives should be ¬b. If the sequence number is not as expected, the protocol entity concludes that the message has been lost and retransmits. In this paper, we will focus on the sender part of ABP protocol. To explain how the tool work. The Sender Part of ABP Protocol: is responsible for accepting messages from the application and sending them via the Medium to the Receiver. The daTA of sender is presented in Figure 6. 6. Conclusion In this paper, we defined Maximality-based Region Graph, also an algorithm generating MRG structure from durational actions Timed Automata (Timed Automata which are coated of Maximality semantics) is presented. The interest of MRG model comes from the fact that it contains information about parallel execution of actions. This allows verification of properties related to true concurrency, in addition to those associated to real-time systems.
As perspective, we will complete this work by the characterization of equivalent behaviors using the temporal maximality bisimulation. Likewase we aim at the reduction of the MRG size for efficient verification by enumeration (modelchecking). 7. References