ICAASE'2014 Maximality-based Region Graph : a Novel Alternative Maximality-based Region Graph: a Novel Alternative Riadh MATMAT Ilham KITOUNI Souad GUELLATI D-Eddine SAIDOUNI, MISC Laboratory, Constantine 2 University, 25000, Algeria {matmat; kitouni; guellati; saidouni}@misc-umc.org Abstract – 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. Keywords – Real time systems, Durational Action Timed Automata, Maximality semantics, Maximality-based region graph. systems. They stick a good balance between expressiveness and tractability and they are 1. INTRODUCTION supported by different verification tools (e.g., KRONOS [19] and UPPAAL [10]). Nowadays, formal verification becomes increasingly used in the industry as a part of the In spite of this, the model suffers from many design process. There is a growing need for problems (decidability, state space explosion...) efficient tools dealing with real aspects of which is impeding its scalability. systems. Many studies have pointed the interest of TA, its Model Checking [11] is one of the most underlying semantic is said the interleaving automated and powerful technique, used when semantics [21]. designing and debugging critical reactive Decidability proof of the reachability problem in systems. It has been extended to real-time TA model is based on a finite abstraction of the systems in which quantitative (timed) set of the clock valuations. The result of this requirements are essential. abstraction is the region graph [2]; it is obtained In general, the system is firstly described using a by the construction of a finite partition of all high level specification models (as timed Petri valuations, with respect of clock constraints. net [12], timed automata [2], the specification is Partitions are also compatible with the then translated to an abstract representation (as progression of time and reset. region graph [2]). This latter is used in several It’s obvious that in real world systems, actions validation methods. are not instantaneous and have durations. This Timed Automata (TA) [2] was proposed to realistic characteristic is important in many specify quantitative requirements expressed by cases. timed constraints [2], they are an extension of Instead of the interleaving semantics, maximality finite state machine with a finite number (but semantics has been proved necessary and arbitrary) clocks in continuous time. TA is very sufficient for carrying both the refinement suitable for modeling and verifying real-time process and action durations [19]. Accordingly, International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 125 ICAASE'2014 Maximality-based Region Graph : a Novel Alternative models based on maximality semantics present Our contribution: In order to preserve all concurrent actions differently from choice [11], achievements of the maximality semantics because of non atomicity of actions. These namely duration of actions and true concurrency, models advocate modeling durational actions we will use the data model and information without splitting them. concerned by the maximality when developing Durational actions timed automata model (daTA) the region graph. We are interested by the was proposed as a timed automata coated by the preservation of the maximality semantics even maximality semantics. daTA model allows to on the abstracted graph of executions of daTA. carry durations of actions and to handle true The fundamental interest of this approach is to concurrency; which are realistic assumptions for propose a structure based on classical regions specifying timed systems. for model checking and all other validation Indeed, to model duration of actions, every edge requirements of concurrent real-time systems of the automaton is annotated by constraints on (possibly distributed).In this paper we expand a clocks. Implicitly constraints on the edges contain theory of region abstraction to capture novel the durations of actions, those that are already aspects which are relevant for verifying true started. In addition, other real-time aspects are concurrency and resulting from the maximality considered (like delaying the start and semantics. deadlines). A single clock is reset on every edge; In fact for the model checking based on daTA it corresponds to the beginning of event (action). model, the range of proprieties to be verified is The termination of an action will be captured by information on locations of the automaton, enlarged to capture actions incompatibility, auto precisely on the destination location of transition. concurrency and the concurrency degree specification [9]. In reality, the action duration is represented by both in the constraints (guards) of the following For this purpose we propose an algorithm for edges and on the next locations and that means generating Maximality-based Region Graph action is not over yet. To better understand these (MRG). We also describe an implementation of principles, consider two actions, if their this algorithm, which allows the construction of executions are dependent, then one should the MRG and its transformation into dotty expect the termination of the other, this will be grammar. Finally, the tool is experimented by realized by the use of the duration of the first means a case study in order to illustrate its action in the guard of the second one. Otherwise functionalities and to show its capabilities to deal they are in concurrency (parallel executions). with real systems. See the example depicted Figure 1. Paper Outline: duration actions timed automata Another important aspect of real-time systems is are recalled in Section 2. Definition and the urgency (i.e., actions whose execution formalization of Maximality based Region Graph cannot be delayed beyond a certain time bound). are proposed in Section 3. Section 4 presents In daTA model urgency is represented by the construction algorithm of MRG with an deadlines as proposed in [17]. The original illustrative example. Section 5 describes the proposition establishes results on timed safety associated tool (TaMaRG) and the major automata [8]. This notification of action's urgency functionalities. Also, a case study is presented is more natural and has the advantage to avoid a and results are commented in this section, lot of cases of time locks [28]. Indeed deadlines namely sender parts of alternative bit protocol. replace invariants as time progress conditions Section 6 concludes the paper and gives some (TPC). Deadlines are clock constraints perspectives on future work. associated directly with edges in the automaton. Thus, in daTA, every state either allows time to pass or allows actions to be executed (i.e., daTA 2. TIMED AUTOMATA WITH DURATION are time-reactive). OF ACTIONS Unfortunately, the region graph of TA doesn’t contain information about durations or parallel 2.1. daTA model execution of actions; those limitations motivate the development of Maximality based Region The daTA model (durational actions timed Graph (MRG) from durational action timed automata) [24] is a timed model defined by a automata. timed transition system over an alphabet representing actions to be executed. This model International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 126 ICAASE'2014 Maximality-based Region Graph : a Novel Alternative takes into account in the specification, the S0 {∅ } duration of actions based on an intuitive idea: , ≔ , ≔ temporal and structural non-atomicity of actions. : ≤ : ≤ : : ≤ This model seems interesting and funneling more and more research because it coats the { ≥ } S1 S2 { ≥ } timed automata model by the maximality , ≔ , ≔ semantics [19]. : ≤ : ≤ : Illustrate this model by an example (Figure 1): : ≤ S3 ≥ , ≥ {∅} , ≔ { ≥ } , ≔ { ≥ } , ≔ ≤ ≤ ≤ S0 S1 S2 : ≥ , ≥ : Figure 1: daTA(A) S4 { ≥ } The duration associated to the action is Figure 2: daTA(B) represented by constraints on the transitions and in the target states of each one. In this sense, The guard of the action becomes ≥ 10 ∧ any enabled transition represents the beginning ≥ 12 . Once this latter is satisfied, can start of the action execution. On the target state of at any time in the enabling open interval transition, a timed expression means that the ∈ [10,+ ∞ [ , ∈ [12,+ ∞ [ , the so called action is possibly under execution. From enabling domain. operational point of view, each clock is Another concept of real time systems is urgency associated to an action. This clock is reset to 0 in our proposal it’s represented as deadlines at the start of the action and will be used in the [8][17]. construction of the temporal constraints as guard We also assume that ⇒ , this condition of the transitions. guarantees that if time cannot progress, at some Fig.1 presents a system of two consecutives state at least one action is enabled from this actions and , the clock is associated to the state. action , on the locality the temporal formula { ≥ 1} represents the duration of the action 2.2. Formalization (which is important to distinguish from invariant in timed automata). In the following ℝ is the set of nonnegative real The end of an action execution is deduced numbers. A clock takes values from ℝ . Given a implicitly in the case of an action that it is set ℋ of clocks, a clock valuation over ℋ is a causally dependent. The action depends on , function assigning a non negative real number to so the transition is guarded by constraint formed every clock. The set of valuations of ℋ noted by duration of and more time {1 ≤ ≤ 2}. V(ℋ ), is the set of total function from ℋ to ℝ . A Starting from this, we can express different valuation is a mapping on ℋ to ℝ . Let be a possibilities of real time systems behaviour like clock, the valuation [ ← 0] resets clock to 0 delaying execution of action or limiting its and each other clock to ( ) . The valuation offering time by manipulation clocks constraints. + maps every clock to ( ) + , ∈ ℝ . Consider another example depicted by Figure 2; Clock constraints over ℋ are defined by the the system consists of two concurrent following grammar: ∷= | |~ | ∧ , processes 1 and 2 synchronizing on an where ∈ ℋ , ∈ ℕand~ ∈ {< ,> ,≤ ,≥ } . The action . The process 1 executes the action satisfaction with respect to clock valuation followed by , while 2 executes then , and function written ⊨ means that according the suppose that actions , and have valuation function , evaluates to true. respectively 10, 12 and 4 units of time as We use (ℋ) to denote the set of clock durations. constraints, ranged over by and also by . In daTA of Fig.2, from the state , the actions We also use a subset of constraints where only and can comply in parallel, and each one can the atomic form of clocks comparison is allowed. finish only if its clock reaches a value equal to its This set is defined by (ℋ ) by the grammar: duration, from where duration condition set ∷= ≥ , where ∈ ℋ and ∈ ℕ. This { ≥ 10, ≥ 12}. subset represents condition duration over a finite set of actions noted . International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 127 ICAASE'2014 Maximality-based Region Graph : a Novel Alternative Definition2.1. A daTA is a 3. DEFINITION OF MAXIMALITY-BASED tuple = ( , ,ℋ , , ) over , where is a REGION GRAPH finite set of states, ∈ is the initial state, ℋ is a finite set of variables named clocks. ⊆ × Characterization of equivalent behavior using (ℋ )× (ℋ )× × ℋ × is a finite set of the temporal maximality semantics and transitions. verification by enumeration (model-checking) Given a transition = ( , , , , , ′) ∈ , must pass through abstractions of durational represents an edge from location to ’ that actions timed automata, that both: launch the execution of action a whenever guard  Generate a finite graph (finite system becomes true. In addition, deadline imposes transitions); an urgency condition: the transition cannot be  Preserve the degree of parallelism; delayed whenever is satisfied, is a clock to  Preserve the system properties. be reset at this transition. Several verification problems such as Finally, : → 2 (ℋ ) is a maximality function reachability analysis, untimed language which decorates each state by a set of timed inclusion, language emptiness as well as timed formula named action durations; these actions bisimulation can be solved by techniques based are potentially in execution on it. ( )= ∅ on the region abstraction [2]. means that no action is yet started. We define Clock Label Occurrence : (ℋ ) → 3.1. Clock regions 2ℋ , as a function which gives clock names occurred in a given timed formulas, recursively An infinite number of distinct valuations can by: verify exactly the same guards in daTA. This ( )= ( )= ∅ observation will serve us to analyze the daTA. ⎧ The restriction on clock constraints that define ⎪ ({ ~ }) = { } the guards and deadlines are used to define a ⎨ ( ∧ ∧…∧ ) = ( ) finite number of equivalence classes of clock ⎪ ⎩ .. valuations (called regions) that can unfold a Such as: duration actions timed automata in a finite ∈ (ℋ ), ∈ ℋ ,∼∈ {< ,> ,≤ ,≥ } and ∈ ℕ . automaton, called Maximality-based Region It is a function which gives clock names occurred Graph (MRG). This property allows algorithmic in a given timed formulas. assessments of the MRG. These valuations Definition2.2. The semantics of a daTA A is a correspond to those of the corresponding infinite timed transition system = ( , ,→ ) automaton. over ∪ ℝ . A state of (or configuration) Notation: for ∈ ℋ , for any ( )∈ ℝ , is a pair (s,v )such as s is a state of A and v is a ( ) denotes the fractional part of , and valuation overℋ , where: ⌊ ( ) ⌋ denotes the integral part of .  = {( , ) | ∈ ∈ ℋ }; Definition3.1. Let = ( , , ,ℋ , ) be a daTA.  = ( , ) such that ∀ ∈ ℋ , ( ) = 0 ; For ∈ ℋ, let be the largest integer c such  →⊆ × ( ∪ ℝ )× consist of the that ( ≤ ) or ≤ is a sub-formula of some discrete and continuous transitions. clock constraint appearing in . The discrete transition is defined for all ∈ by The equivalence relation ≅ is defined over the 1= ,, ,,, ∈ ⊨ . set of all clock interpretations for ℋ; v ≅ v′ iff all ( ,) ⎯⎯ ( , [ ≔ ]) the following conditions hold: The continuous transition is defined for all ∈ i. For all ∈ ℋ, either ⌊ ( ) ⌋ and ⌊ ′( ) ⌋ ∈ℝ ∀ , ⊨ () are the same, or both ( ) and ( ) are ℝ by 2= , where ( , ) ⎯⎯ ( , ) greater than . ( ) = ¬⋁( |∃ ∈ : = ( , , , , , ′)) is ii. For all , ∈ ℋ with ( ) ≤ and the time progress condition in [7] [13]. ( )≤ , ( ) ≤ ( ) iff , ,, Rule 1 states that an edge s ⎯⎯⎯ s′ defines a ′( ) ≤ ′( ) . discrete transition from current location iii. For all ∈ℋ with ( )≤ , whenever the guard holds in current valuation ( ) = 0 iff ′( ) = 0. and clock is reset to 0. According to 2, time The equivalence relation ≅ is defined over the can progress in only when ( ) is true, that set of all clock interpretations for ℋ. We will use is as long as no deadline of an edge leaving s [ ] to denote the equivalence classes of V(ℋ )to becomes true. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 128 ICAASE'2014 Maximality-based Region Graph : a Novel Alternative which belongs. It also clock regions denoted function). The function ( , ) presented in by: = ] = { ′ ∈ (ℋ )| ≅ ′}. [ definition 3.2 ensures this feature. Example 3.1. Consider a daTA with two clocks The transitions relation of ( ) is an and with = 2 and = 1. 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 1 if in daTA a transition of the form ( , , , , , ) ∈ . As usual the transitions relation can be defined using a successor 0 function over the clock regions and some 1 2 maximality functions. Definition3.2. Let = ( , , ,ℋ , ) be a daTA. Figure 3: Clock regions The Maximality-based Region Graph associated to A is ( )= , 0, , where: The clock regions shown in Figure 3 are:  14 open line segments: e.g. [0 < = i. , is a set of states regions having the < 1]; form ( , ) with ∈ and is a region.  8 open regions: e.g.[0 < < < 1] ; ii. = ( , ), is the initial state region,  6 corner points: e.g.[ = 1, = 1] . where s is the initial state for and We call end-region the region satisfying the = [ ( )] such as ∀ ∈ ℋ , ( ) = 0. following condition: ∀ , ∈ ℋ ⇒ > . The end iii. ∶ × → 2 ℋ , is a maximality region is open to infinity on all clocks region. It function assigning to each state region does not have a successor region, in Figure 3 ( , ) a finite set of clocks representing the end-region is [x > 2, > 1]. maximal event names. It’s defined as: ( , ) = { | ≥ ∈ ( )} . 3.2. Successor function iv. The transition relation is defined by two kinds of transitions: Let and ′ be regions. The region ′ is a  Passage of time. Each region( , ) , successor of , noted ( ) = ′ iff ∀ ∈ ⇒ where is not an end class, has an ∃ ∈ ℝ and + ∈ ′. edge to its successor( , ( )) . Now we are ready to define the Maximality- based Region Graph associated to a daTA Formally we write: = ( , , ,ℋ , ) . ⊨ ( )∧ ( )⊨ () ( , ) (, ( )) 3.3. Regions Graph Coated of Maximality  Transition of . Given a region( , ) , for Let ( ) be a Maximality-based Region each transition =( , , , , ,′ )∈ , Graph of a daTA A. Similar to region automaton there is an edge to ( , ′) where: [2], a state of ( ) records the state of = [ ≔ 0], ⊨ and ⊨ ( ′) . the timed transition of , and the This is formalized by the rule: , ,, equivalence class of the current values of ⎯⎯⎯ ∧ ⊨ ∧ [ ≔ 0] ⊨ ( ′) the clocks, but also it conserve the information ( ), , of actions under execution. It is of the form ( , ) ( , ) ⎯⎯⎯⎯⎯⎯⎯⎯ ( , [ ≔ 0]) with ∈ and is a clock region. The Maximality-based Region Graph starts in some state ( , ). 4. Generating Maximality-based Region According to the maximality semantics and the Graph daTA structure, each state of Maximality-based Region Graph contains a set of clocks which In this section we propose an algorithm which corresponds to events for actions under constructs the Maximality-based Region Graph executions. Those events are captured by timed for durational actions timed automata. It is based formulas initially on states of daTA (delivery by on the successor function and maximality semantics to create new regions by using the daTA structure. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 129 ICAASE'2014 Maximality-based Region Graph : a Novel Alternative The Algorithm: Initially the daTA is traversed so Output : Maximal-based Region Graph correspondi ng toA as to find for each clock ∈ ℋ. This is required for abstraction and ensuring finite 1: calculate for each clock ∈ ℋ . number of states regions in the MRG. After 2: let be the initial state region of MRG ; creating initial state region of MRG, the 3: (P ←, ∅; ) algorithm calculates the successor regions. 4: enqueue(P; l ); // = ( , ) Regions are specified by one of three forms (type_1, type_2, type_3). 5: whileP not empty do 6: = dequeue( ); // = (,) The function returns a successor of current region. In this step the algorithm checking under 7: if isnotend region then the successor region guard and TPC of daTA for 8: Switch type_region( ) creating regions states and transitions, the 9: case type_1: ’ = (, _1); regions states are creating with keeping all actions under execution, this is performed by the 10: case type_2 :’ = (, _2); function , the transitions are created either by 11: case type_3 :’ = (, _3); passage of time(delay transitions) or by actions 12: if ⊨ ( )∧ ( )⊨ ( ) then (discrete transitions). 13: = (, ) Delay transition is created if the current region 14 ( ′) ≔ { | ≥ ∈ ( )} and its successor satisfies the TPC, while discrete transitions is created if the region 15: add ′to ; satisfies the guard and satisfies the TPC, in this 16: add to ; case, we keep (on the transition) clock 17: associated with the action and clocks ∶ → ′; corresponding to actions under execution. Recall 18: enqueue( ; ′); that those actions condition the launching of 19: end if current transition. This is performed by the 20: for all =( , , , , , ) do function . 21: if ′⊨ ∧ ′ [ ≔ 0] ⊨ ( ) then On states regions the function ( , ) is 22: = ( , [ ≔ 0] ′); constructed, to capture the maximal events and 23 ( )≔{ | ≥ ∈ ( )} to ensure maximum information on concurrency. The MRG generated by this algorithm 24: add to ; correspond to daTA of Figure 1, is represented 25: ( ), , : ⎯⎯⎯⎯⎯⎯⎯⎯ ; by Figure 4. 26: add to ; 27: enqueue( ; ); 28: end if 29: end for 30: end if 31: end while 5. Implementation and case studies 5.1. Implementation TaMaRG is a tool for generating Maximality- based 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 Figure 4: MRG correspond to daTA (A) functional view is sketched in Figure 5. Algorithm 1 Construction of Maximal -based Re gion Graph Input : durational actions timed automata A International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 130 ICAASE'2014 Maximality-based Region Graph : a Novel Alternative 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. daTA Graphical Editor TaMaRG MRG-Generator tool MRG-Dotty Adaptor MRG Figure 5: Functionalities of TaMaRG tool 5.2. Case studie Figure7: Part of MRG of daTA of sender part of ABP ABP Protocol: ABP (Alternating Bit Protocol) is a connection-less protocol for transferring The Model: The alternating bit protocol consists messages in one direction between a pair of of a sender S, a receiver R, a channel K from S protocol entities. It is a simple form of the Sliding to R and a channel L from R to S, its architecture Window Protocol with a window size of 1 [23], is as follow: [16] .The name of this protocol stems from the fact that each message is augmented with an The sender S and receiver R communicate via additional bit. This protocol uses one-bit the same lossy communications mediums (L and sequence number (which alternates between 0 K). So messages may be lost. The basic and 1) in each message and an acknowledgment principle is to stamp messages with a one bit to determine whether the message must be sequence number. When a protocol entity sends retransmitted. message (either Data or Acknowledgment) with sequence number b. The next message it The aim of this section is to illustrate the use of receives should be ¬b. If the sequence number daTA tool; we will focus on sender part. 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. Table 1: MRG Result for ABP Protocol S R K L State 151 224 276 152 Transition 195 261 361 198 6. Conclusion In this paper, we defined Maximality-based Figure 6: daTA of sender part of ABP protocol Region Graph, also an algorithm generating International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 131 ICAASE'2014 Maximality-based Region Graph : a Novel Alternative MRG structure from durational actions Timed [11] H. Bowman and R. Gomez: Concurrency Automata (Timed Automata which are coated of Theory, Calculi and Automata for Modelling Untimed and Timed Concurrent Systems. Maximality semantics) is presented. The interest ISBN-10: 1-85233-895-4 ISBN-13: 978-1- of MRG model comes from the fact that it 85233-895-4 Springer-Verlag, 2006. contains information about parallel execution of [12] R. Barbuti, N. De Francesco, L. Tesei : actions. This allows verification of properties Timed Automata with non-instantaneous Actions. Fundamenta Informaticae 46 (2001) related to true concurrency, in addition to those 1–15 1, IOS Press, 2001. associated to real-time systems. [13] J.F. Groote, J. Springintveld,“Focus points and convergent process operators”. A proof As perspective, we will complete this work by the strategy for protocol verification, In Journal characterization of equivalent behaviors using of Logic and Algebraic Programming, the temporal maximality bisimulation. Likewase 49(1/2):31{60}, 2001. we aim at the reduction of the MRG size for [14] Holton, D. R. W., “A PEPA Specification of efficient verification by enumeration (model- an Industrial Production Cell”, In The Computer Journal, vol. 38 (7), pp. 542-551, checking). 1995. [15] K. Bouaroudj, DE. Saidouni, and I. Kitouni, “Testing Stochastic Systems Using MoVoS 7. References Tool: Case Studies”. T. Skersys, R. Butleris, [1] R. Alur,C. Courcoubetis and D. Dill, “Model- and R. Butkiene (Eds.): ICIST 2013, CCIS Checking in Dense Real- Time”. Information 403, pp. 310–321, Springer-Verlag Berlin and Computation, 104(1) : 2–34, 1993. Heidelberg, 2013. [2] R. Alur, and D. Dill,“A Theory of Timed [16] A. Hessel, K. Larsen, B. Nielsen, P. Automata”,In Theoretical Computer Science Pettersson, andA. Skou, “Time-optimal real (TCS),vol. 126(2), pp. 183–235, 1994. time test case generation using UPPAAL”, In FATES’03, Montreal, October 2003. [3] C. Baier, J-P. Katoen,“Principles of Model [17] R. Gómez, “Model-checking timed automata Checking”; The MIT Press Cambridge, with deadlines with Uppaal”. Formal Aspects Massachusetts, London, England: ISBN of Computing, vol 25 (2), pp 289-318, 2013. 978-0-262-02649-9, 2008. [4] H. Bowman, Time and action lock freedom [18] S. Guellati, I. Kitouni, and D.E. Saidouni, properties for timed automata. In “Verification of durational action timed Proceedings of FORTE 2001, 119–134, automata using UPPAAL”, In International 2001. Journal of Computer Applications (IJCA), vol. 56 (11), pp. 33-41, Published by [5] A. Burns, “how to verify a safe real time: the Foundation of Computer Science, New York, application of model checking and timed USA, October 2012. automata to the production cell case study”, [19] S. Yovine, “ Kronos:A verification tool for In Real time Systems journal, vol. 24(2), pp. real-time systems”, InInternational Journal of 135-152, 2003. SoftwareTools for Technology Transfer, 1(1- [6] R. Alur, L. Fix, and T. A. Henzinger. Event- 2), pp. 123–133, 1997. clock automata: a determinizable class of [20] D.E. Saїdouni, and N.Belala, “Actions timed automata. Theoretical Computer duration in timed models” In Proceedings of Science, 211(1–2):253–273, 1999. International Arab Conference on [7] H. Bowman and R. Gomez: Concurrency Information Technology (ACIT’2006), Theory, Calculi and Automata for Modelling December 19-21th 2006. Untimed and Timed Concurrent Systems. [21] D. E. Saïdouni , J. P. Courtiat, “ Prise en ISBN-10: 1-85233-895-4 ISBN-13: 978-1- Compte des Durées d’Action dans les 85233-895-4 Springer-Verlag, 2006. Algèbres de Processus par l’Utilisation de la [8] T.A. Henzinger, X. Nicollin, J. Sifakis, & Sémantique de Maximalité” , In CFIP. 2003, S.Yovine, “Symbolic model checking for Hermes, France, 2003. realtime systems”. Inf. & Comp., [22] S. Tyszberowiez, “How to implement a 111(2):193–244, 1994. safe real-time system : The OBSERV [9] S. Guellati, I. Kitouni, R. Matmat and D.E. implementation of the production cell case Saidouni, “Timed Automata with Action study” In Real time Systems, vol. 15(1), pp. Durations - From Theory to Implementation”, 61-90, 1998. In the 20th International Conference on [23] K.H. Talukder,“ Formal verification of the Information and Software Technologies Alternating Bit Protocol”, In 6th (ICIST 2014), Kaunas, Lithuania, G. International Conference on computer & Dregvaite and R. Damasevicius (Eds.): Information Technology (ICCIT), 2003. ICIST 2014, CCIS 465, pp. 94-109, 2014. Springer International Publishing [24] I. Kitouni, H. Hachichi, K. Bouaroudj, and Switzerland 2014. (Accepted to be D.E. Saidouni, “Durational Actions Timed published). Automata:Determinization and [10] G. Behrmann, A. David, and K. Larsen. “A Expressiveness”, In (IJAIS), vol. 4(2), pp. 1- tutorial on Uppaal”. In SFM-RT 2004, LNCS 11,Published by Foundation of Computer 3185,pages 200–236. Springer, 2004. Science, New York, USA, September 2012. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 132