Synthesis of Parametric Embedded Real-Time Systems

全文

(1)Synthesis of Parametric Embedded Real-Time Systems Pao-Ann Hsiung Institute of Information Science, Academia Sinica, Taipei, Taiwan, ROC. E-mail: [email protected]. Abstract Synthesis means restricting a specification behavior such that the synthesized behavior satisfies some given property. Previous work on the synthesis of embedded real-time system have not considered parameters. In the world of embedded systems, parameters are of paramount importance for system design because tradeoffs among various system features and functionalities have to be made. We define and solve the parametric embedded real-time system synthesis problem by integrating parametric analysis techniques into embedded real-time system synthesis. An example is given to illustrate the feasibility of our approach. Keywords: embedded real-time system synthesis, parametric analysis, parametric synthesis, formal design. 1 Introduction Currently, a technological gap exists between system analyzers and system designers because the former do not take real-world constraints into consideration while verifying systems and the latter often lack preciseness and completeness in designing systems. Researchers are trying to bridge this gap through formal synthesis techniques [4, 5, 6, 11] and through practical analysis techniques [2, 7, 8, 10, 9, 15]. Our effort at incorporating system parameters into embedded real-time system synthesis is also directed towards this goal. On one hand, parametric analysis techniques have been proposed for real-time systems [15]. On the other hand, synthesis methods have been proposed for real-time systems [5, 12, 16] through extensions of Ramadge & Wonham’s classical work [13] on supervisor synthesis. Our work consists of integrating these two classes of techniques such that embedded real-time system can be synthesized for systems with static parameters. In general, system parameters include system component costs and performance readings such as response time, throughput, utilization, power (percentage throughput per unit utilization), fault-tolerance, scalability, reliability, and others. These parameters become all the more important in embedded systems, because the behavior of an embedded. system is constantly under the influence of an environment. Synthesis that does not consider the values of such parameters may not give the best system design result. Parametric analysis of real-time systems solves the problem of finding a general relationship that valuations for a set of parameters must satisfy in order for a system to meet a given property [15]. Parameters appear in a system description and as a quantification suffix in a property specification. Previous work [15] first modeled a system by Parametric Timed Automata (PTA), specified a system property by parametric timed computational tree logic (PTCTL), and then derived a condition on parameter valuations, which is a boolean combination of semi-linear expressions. Synthesis for embedded control systems was mainly performed in the discrete time domain, with a large portion of classical work done by Ramadge and Wonham [13, 14]. Around 1994, when timed automata was proposed as a dense-time model for real-time systems [3], discrete synthesis was extended to dense real-time systems [4, 12, 17] as well as to hybrid systems [16]. Recently, the same technique was further extended to multimedia scheduler synthesis [1]. Given a dense real-time system modeled by timed automata and a (temporal) property given as a formula in Timed Computation Tree Logic (TCTL) [2, 8], a restriction of system behavior is synthesized for satisfying the property. This is called embedded real-time system (ERTS) synthesis problem. In previous work on synthesis [1, 4, 5, 12], discrete variables and constants appear in both system description and property specification, but parameters were not allowed. We extend the existing work by allowing parameters to appear in system description and property specification such that embedded real-time system can be synthesized for parametric systems, too. This article is organized as follows. Section 2 formulates and models the Parametric Embedded Real-Time Systems (PERTS) synthesis problem. Section 3 proposes a method for solving PERTS synthesis problem. Section 4 illustrates the proposed method through an application example. Section 5 concludes the article..

(2) 2 Problem Formulation The problem that we are modeling and solving here consists of two main issues: 1. Parameter Valuation: Given a system, a specification, and a set of parameters, find a general condition on the parameter values such that the system satisfies the specification. 2. Embedded Real-Time System Synthesis: Given a system, a synthesis mask, and a specification, find a restriction of the system behavior, interpreted under the given mask, such that it satisfies the specification. Given a system, a synthesis mask, a specification, and a set of parameters, both of the above two issues must be solved. A synthesis mask is a boolean vector that specifies which transitions are synthesizable and which are not. These two issues may at first appear to be orthogonal problems due to the former being a static problem (parameter values do not change with time), while the latter a dynamic problem (restricts the dynamic behavior of a system). But, they are in fact intricately involved with each other. The following are two ways in which they affect each other.. . Static affects dynamic: Corresponding to different static parameter valuations, a system description will have different interpretations, which results in different behavior synthesized. Dynamic affects static: When the dynamic behavior of a system is restricted in some way, certain static parameter valuations that worked originally may no longer work now, where work means allowing a system to satisfy a given property specification.. Due to the above relationships between the two issues, we need to find the most general condition on parameter valuations while imposing the minimum restriction on a system behavior to satisfy a given specification. Before formulating our problem, some models and definitions are necessary. Our target is a real-time system, that is, a system whose correctness depends on satisfying certain temporal constraints. Here, a real-time system is formally modeled by Parametric Timed Automaton (PTA) model [15]. The PTA model basically extends Timed Automata (TA) [3] with parameters in the system description. Timed automata are automata with time or clock variables, which model temporal characteristics and temporal specifications. In the following, the set of integers and non-negative real numbers are denoted by N and R0 , respectively. Mode predicates are used to specify transition triggering conditions and mode invariants and are defined as follows.. Definition 1 : Mode Predicate Given a set C of clock variables, a set D of discrete variables, and a set H of parameters, the syntax of a mode predicate over C , D, and H is defined as: := false j x c j x ; y c j d c j i ai i c j 1 ^ 2 j :1 , where x; y 2 C , 2 f; <; =; ; >g, c; ai 2 N , i 2 H , d 2 D, and 1 ; 2 are mode predicates. Let B (C; D; H ) be the set of all mode predicates over C , D, and H . A PTA is composed of various modes interconnected by transitions. Variables are distinguished into clock and discrete, where variables of the former type increment at a uniform rate and can be reset on a transition, while variables of the latter type change values only when assigned a new value on a transition. Definition 2 : Parametric Timed Automaton A Parametric Timed Automaton (PTA) is a tuple A = (M; m0 ; C; D; H; ; E; ; ) such that: M is a finite set of modes, m0 2 M is the initial mode, C is a set of clock variables, D is a set of discrete variables, H is a set of static parameters, : M 7! B (C; D; H ) is an invariance function that labels each mode with a condition true in that mode, E M M is a set of transitions, : E 7! B (C; D; H ) defines the transition triggering conditions, and : E 7! 2C [(DN ) is an assignment function that maps each transition to a set of assignments such as resetting some clock variables and setting some discrete variables to specific integer values. Definition 3 : Interpretation An interpretation, I , of a PTA A = (M; m0 ; C; D; H; ; E; ; ) is a mapping from the set of parameters H to the set of integers N . A PTA A interpreted under an interpretation I will be denoted as AjI . Definition 4 : State Given a PTA A = (M; m0 ; C; D; H; ; E; ; ), a state s of A is defined as a mapping from C [ D to R0 [ N such that 8x 2 C; s(x) 2 R0 is the reading of clock x in s, and 8d 2 D; s(d) 2 N is the value of d in s. Definition 5 : Satisfaction of Mode Predicates The satisfaction of mode predicates by a state s under interpretation I , written as s j=I , is defined by the following rules: s 6j=I false; s j=I x ; y c iff s(x) ; s(y) c; s j=I x c iff s(x) c; s j=I d c iff s(d) c; s j=I ai i c iff ai I ( i ) c; s j=I 1 _ 2 iff s j=I 1 or s j=I 2 ; and s j=I :1 iff s 6j=I 1 .. P. P.

(3) Given a PTA A = (M; m0 ; C; D; H; ; E; ; ), an interpretation I for H , and a state s, let sM be the mode in M such that s j=I (sM ). If there is no mode m 2 M such that s j=I (m), then sM is undefined. Definition 6 : Mode Transition Given two states s; s0 , there is a mode transition from s to s0 in A under interpretation I , in symbols s !I s0 , iff 0 M M Both s0 ; s are defined, (sM ; s M ) 2 E0 , s j=I (sM ; s M ), and. . 8x 2 C (x 2 (sM ; s M ) ) s0 (x) = 0) ^(x 62 (sM ; s M ) ) s0 (x) = s(x)) . Also, given a state s and a 2 R , let s + be the state that agrees with s in every aspect except for all x 2 C , 0. 0. 0. s(x) + = (s + )(x).. Definition 7 : Interpreted PTA A PTA A = (M; m0 ; C; D; H; ; E; ; ) is said to be interpreted under some interpretation I , when all the mode invariants and trigerring conditions on transitions have their parameters interpreted under I , i.e., 8 2 H , is replaced by I ( ) 2 N . When A is interpreted under I , it is denoted by Aj I . Let VH; be the set of all possible valuations of the parameters in H and of those appearing in a PTCTL formula . Definition 8 : A Feasible s-run Given a state s of PTA A = (M; m0 ; C; D; H; ; E; ; ) under interpretation I , a computation of A starting at s is called a feasible s-run which can be represented by an infinite sequence ((s1 ; t1 ); (s2 ; t2 ); : : : : : :) such that s = s1 ; and for each t 2 R0 , there is an i 2 N such that ti t; and for each integer i 1, sMi is defined and for each real 0 ti+1 ; ti , si + j=I (sM i ); and for each i 1, A goes from si to si+1 because of - mode transition, i.e., ti = ti+1 ^ si !I si+1 ; or - time passage, i.e., ti < ti+1 ^ si + ti+1 ; ti = si+1 . We denote by Run(AjI ) the set of all feasible s-runs of a PTA A interpreted under I . Timed Computation Tree Logic (TCTL) [8] is extended to include static parameters in the automata and parameters in TCTL formula, we call this extension Parametric Timed Computation Tree Logic (PTCTL). The syntax of a PTCTL formula, , used for analyzing models described by a PTA A = (M; m0 ; C; D; H; ; E; ; ) is defined as follows. Definition 9 : Parametric TCTL (PTCTL) A PTCTL formula is defined to have the following syntax.. ::= j 91 U 2 j 81 U 2 j 1 _ 2 j :1. (1). where is a mode predicate, 1 , 2 are PTCTL formulae and is either an integer constant in N or a parameter in H . Note that the parameter subscripts of modal formulae can also be used as parameters in PTA. Definition 10 : Synthesis Mask A synthesis mask c maps each transition of a PTA into a boolean value, such that true (1) denotes a synthesizable transition, and false (0) denotes an unsynthesizable transition. c : E ! f0; 1g (2) where E is a set of transitions of some given PTA. Often, a synthesis mask is simply given as a boolean vector, c (E ) = hc (e0 ); c (e1 ); : : : ; c(ejEj )i, assuming some sequential order for all the transitions in a PTA. Given the above formal definitions and notations, our target problem is thus formulated as follows.. Definition 11 : PERTS Synthesis (PSynth(S; c ; )): Given a real-time system modeled by a parametric timed automaton S , a synthesis mask c , and a parametric timed computation tree logic formula , the parametric embedded real-time system synthesis problem is to find a general condition V on the parameter valuations and a synthesized parametric timed automaton SC such that the following conditions are satisfied. 1. the synthesized system SC , interpreted under V , satisfies , that is, SC j=V , and. 2. there is no state s 2 QS such that s is reachable in S jv , s 2= QSC and s j=v for some parameter valuation v 2 VH; , where S jv is the interpretation of S under v, QS and QSC are the state-spaces of S and SC , respectively.. 3 PERTS Synthesis As mentioned at the start of Section 2, we have two goals in solving the parametric controller synthesis problem: (1) derive most general conditions on parameter valuations, and (2) construct a minimally restricted synthesized system satisfying a given property. These two goals are inter-related. To achieve these two goals simultaneously, we propose an integrated approach, where the iterative algorithm of embedded real-time system synthesis is the basis and parametric analysis is performed on-the-fly.. 3.1 Parametric Analysis Parametric analysis is a method for finding a general condition on the valuation of parameters appearing in a system and in a specification such that the given system satisfies the given specification [15]. Given a system represented by a PTA S = hM; m0 ; E; X; Y; H; L; ; ; ; i.

(4) Table 1: Labeling Algorithm for Parametric Analysis PAnalyze(S; ) PTA S = hM; m0 ; E; X; Y; H; L; ; ; ; PTCTL Formula ;. f. i;. Construct Param. Region Graph GS : = (R; F ); (1) for each r 2 R, recursively compute label L (r); (2) return r0 2R0 L (r0 ); (3) // R0 R is a set of all initial regions in R. W. g. and a PTCTL specification , parametric analysis finds a condition VH; on the valuation of parameters in H and of those appearing in such that S j=VH; . The condition VH; is a boolean combination of semi-linear expressions, where each semi-linear expression gives the pattern of values that a parameter could take. A semi-linear expression is a union of a finite number of integer sets like fa + b1j1 + b2 j2 + : : : + bn jn j j1 ; : : : ; jn 2 Ng for some a; b1 ; b2; : : : ; bn 2 N . Parametric analysis is given briefly in Table 1 as a function PAnalyze(). The basic steps are explained here, but details can be found in [15]. First, parametric analysis constructs a parametric region graph, which is a parametric extension of region graphs proposed by Alur et al. [3]. All the states in a region have the same truth value with respect to model checking and hence can be taken as the basis of parametric analysis. Second, a conditional path graph is constructed for each pair of regions in the parametric region graph. A conditional path graph for a pair of regions represents a predicate condition and a semi-linear expression such that a computation run along that path must satisfy the predicate condition and takes time as recorded by the semi-linear expression. Third, through a labeling algorithm each region r is associated with a label L (r) representing S; r j=L (r) . The labels are computed recursively. Finally, a disjunction of labels associated with all initial regions is taken as the general parametric condition for the satisfaction of by system S .. 3.2 Predicate Synthesis Predicate synthesis modifies existing triggering condition predicates on synthesizable transitions and invariant predicates in modes of a given to-be-controlled system such that the resulting modified system satisfies a given specification. More formally, given a system represented by a PTA S = hM; m0 ; E; X; Y; H; L; ; ; ; i interpreted under a parametric valuation V , a synthesis mask c , and a PTCTL specification , predicate synthesis constructs a new PTA. Table 2: System Synthesis Algorithm (2 Timed Game) Synthesize System(S jV ; c ; ) PTA S = hM; m0 ; E; X; Y; H; L; ; ; ; i; V is an interpretation or parameter valuation; Synthesis Mask c : E ! ftrue; falseg; PTCTL formula ;. f. g. z0 = ; for i = 0; 1; : : : f zi+1 = zi \ (zi ; ); if (zi+1 = zi ) break; g SC = Synthesize Predicate(S jV ; c; zi ); return SC ;. (1) (2) (3) (4) (5) (6). zi is a set of states, i 0, and SC is a PTA.. SC by refining (e) for all e 2 E with c (e) = true, and by refining (m) for all m 2 M , such that SC ; r j=V , for all regions r in the parametric region graph of S C . The algorithm Synthesize System() given in Table 2 illustrates how a system PTA is synthesized. The basic steps are explained here, but details can be found in [4, 5]. First, a fix-point is obtained iteratively, which represents a closure of all the regions (collection of states) in which can be satisfied. The iteration starts with an initial region z0 which includes all states that satisfy . In each iteration i, a predecessor operator is applied to region z i and a new region zi+1 is obtained by an intersection of zi and (zi ; ) (for 2 timed game) or by a union of z i and (zi ; ) (for 3 timed game). Here, a timed game is simply a PTCTL formula. The new region represents a 1-step backward reachable collection of states. Then, using the resulting fix-point zi , predicates are synthesized by the algorithm Synthesize Predicate() given in Table 3. The predicate synthesis algorithm is given as a function Synthesize Predicate() in Table 3. Here, the predicates we are concerned with are those appearing in triggering conditions on synthesizable transitions and those appearing in invariant conditions of modes. By predicate synthesis, we mean the existing predicates in a system S are to be modified into new predicates, called synthesized predicates, which guarantee that the modified system SC satisfies . This algorithm uses a region, z , called the fix-point region which is a closure of regions that satisfy . First, for all modes m in M that has a state in z , its invariant condition (m) are conjuncted with z so as to restrict the states in each such mode to only those in z . Then, for all out-going synthesizable transition e of each such mode m, its triggering condition (e) is conjuncted with a predicate condition . This predicate condition ensures that for each unsyn-.

(5) Table 4: PERTS Synthesis Algorithm (2 Timed Game). Table 3: Predicate Synthesis Algorithm Synthesize Predicate(S; c; z ) PTA S = hM; m0 ; E; X; Y; H; L; ; ; ; Synthesis Mask c : E ! ftrue; falseg; Set of regions z ;. f. for each m 2 M s.t. 9s 2 z; sM. (m) = (m) ^ z ;. =mf. for each out-going trans e of m with c (e) = true f. gg g. PSynth(S; c ; ) PTA S = hM; m0 ; E; X; Y; H; L; ; ; ; Synthesis Mask c : E ! ftrue; falseg; PTCTL formula ;. i; (1) (2). f. (3). (e) = (e) ^ 0 ; (4) 0 0 where = 8 e 2 E 1 0 ( (e0) = false) ^ ( (e0 ) ) z) c @ ^ 9 a run h(s0 ; t0); (s1; t1 ); : : : ; (sk ; tk )i A M M M such that e0 = (sM 0 ; s1 ); e = (sk;1 ; sk ):. return S ;. g. Lemma 1 A feasible computation run cannot simultaneously belong to two sets of runs of S interpreted under two contradictory parameter valuations. Theorem 1 Completeness There does not exist a state s 2 and a parameter valuation v 2 VH; such that s is. QS. (1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11). zi is a parametric region, i 0, VH; VH; is a condition on parameter values, SC : PTA.. 3.3 PERTS Synthesis Algorithm We propose a solution to the PERTS synthesis problem by an integration of the iterative synthesis algorithm (described in Table 2 and the parametric analysis algorithm (described in Table 1. The basis is the synthesis algorithm and parametric analysis is performed on-the-fly. Parametric regions are labeled as and when they are included into the fix-point set of regions derived in each iteration. Here, labeling regions means regions are associated with conditions on parameter valuations such that computation runs starting from those regions satisfy a given specification under the associated conditions. The algorithm for this approach is given as function PSynth() in Table 4, where a system PTA S is given along with a synthesis mask c and a PTCTL property . On-thefly parametric analysis, as represented by OTF PAnalyze() in Table 5, is performed in each iteration (Step (4) of Table 4). A restricted behavior is synthesized in Step (9) using the fix-point region zi . In the rest of this subsection, we will state the completeness and termination of the iterative algorithm. Proofs are omitted due to page-limits.. Construct Param. Region Graph GS : = (R; F ); z0 = ; for i = 0; 1; : : : f OTF PAnalyze(zi ; ); zi+1 = zi \ (zi ; ); if (zi+1 = zi ) break; g if (R0 6= ;) f // R0 zi is a set of initial regions of S VH; = r0 2R0 L (r0 ); SC = Synthesize Predicate(S jVH; ; c ; zi ); return (VH; ; SC ); g else return (false, NULL); // No solution. W. (5). thesizable transition f (i.e., c (f ) = false), the behavior of a run from f to e does not leave the fix-point region z .. i;. Table 5: On-the-Fly Parametric Analysis Algorithm OTF PAnalyze(Z; ) Set of Parametric Regions Z ; PTCTL Formula ;. f. g. for each r. 2 Z , recursively compute label L (r);. (1). reachable in S jv , s 2 = QSC , and s j=v , where QS and QSC are respectively the state spaces of a system S and its corresponding controlled system SC derived using the iterative parametric controller synthesis algorithm. Theorem 2 Termination The iterative parametric controller synthesis algorithm is guaranteed to terminate.. 4 Application Experiment The proposed PERTS synthesis method is applied to an example: a 3 timed-game. This example illustrates how the proposed method for parametric embedded real-time system synthesis works and how syntheses of trigger predicates on a transition correspond to prunings of a parametric region graph. A system PTA for this example is given in Fig. 1 and.

(6) x=0. . Iteration i = 0: In Step (4), regions in z 0 are labelled with parametric conditions as follows L(r1 ) = ( = 1 ^

(7) < 3 ^ 1 3), L(r2 ) = ( = 1 ^

(8) < 3 ^ 1 2), L(r3 ) = ( = 1 ^

(9) < 3 ^ = 1), L(r4 ) = ( 6= 1 ^

(10) 3 ^ 1 3), L(r5 ) = ( 6= 1 ^

(11) 3 ^ 1 2), L(r6 ) = ( 6= 1 ^

(12) 3 ^ = 1), L(r7 ) = (1 2), L(r8 ) = (1 2), and L(r9 ) = ( = 1). In Step (5), the next fix-point region space is computed as z1 = fr1 ; : : : ; r9 ; r10 ; : : : ; r18 g.. . Iteration i = 1: In Step (4), new regions in z 1 are labelled with parametric conditions as follows L(r10 ) = L (r1 ), L(r11 ) = L (r2 ), L(r12 ) = L (r3 ), L(r13 ) = L (r4 ), L(r14 ) = L (r5 ), L(r15 ) = L (r6 ), L(r16 ) = L (r7 ), L(r17 ) = L (r8 ), L(r18 ) = L (r9 ). In Step (5), the next fix-point region space is computed as z2 = fr1 ; : : : ; r18 ; r19 ; : : : ; r27 g.. . Iteration i = 2: In Step (4), new regions in z 2 are labelled with parametric conditions as follows L(r19 ) = ( = 1 ^

(13) < 3 ^ 2 4), L(r20 ) = ( 6= 1 ^

(14) 3 ^ 2 4), L(r21 ) = L (r13 ), L(r22 ) = L (r14 ), L(r23 ) = L (r15 ), L(r24 ) = 2 4, L(r25 ) = L (r16 ), L(r26 ) = L (r17 ), L(r27 ) = L (r18 ). In Step (5), the next fix-point region space is computed as z3 = fr1 ; : : : ; r27 ; r28 ; : : : ; r32 g.. . Iteration i = 3: In Step (4), new regions in z 3 are labelled with parametric conditions as follows L(r28 ) = ( = 1 ^

(15) < 3 ^ 3 5), L(r29 ) = ( 6= 1 ^

(16) 3 ^ 3 5), L(r30 ) = L (r20 ), L(r31 ) = 3 5, L(r32 ) = L (r24 ). In Step (5), the next fix-point region space is computed as z4 = fr1 ; : : : ; r32 ; r33 ; : : : ; r36 g.. . Iteration i = 4: In Step (4), new regions in z 4 are labelled with parametric conditions as follows L(r33 ) = ( = 1 ^

(17) < 3 ^ 4 6), L(r34 ) = L (r29 ), L(r35 ) = 4 6, L(r36 ) = L (r31 ). In Step (5), the next fix-point region space is computed as z5 = fr1 ; : : : ; r36 ; r37 ; : : : ; r40 g.. . Iteration i = 5: In Step (4), new regions in z 5 are labelled with parametric conditions as follows. M0 = 1^. x=1 x := 0 6= 1^ = 3^ x>3 x>7 M1 M2 M3

(18) < 3^ x4. M4.

(19) 3 ^

(20) = 9^ x<8 x>8 x := 0. M5. Figure 1: System PTA S for Example 1 the PTCTL specification for this example is as follows.. = 93< (M5 ^ x 5 ^ x 7). (3). where is a parameter, M5 is a mode name, and x is a clock variable. For simplicity, it is assumed that all transitions are synthesizable. The PERTS synthesis algorithm given in Section 3.3 was used to synthesize a system PTA S illustrated in Fig. 1 such that it satisfied the PTCTL specification given in Equation (3). A parametric region graph G S : = (R; F ) was constructed, whose pruned version is shown in Fig. 2. Just as a complete parametric region graph depicts the behavior of a system PTA S , a pruned parametric region graph depicts the behavior of a controlled system PTA SC . A pruning in the graph is depicted as a dashed bold arrow and represents a control synthesis (refinement) of trigger predicates on some transition. A parametric region is represented by an oval in Fig. 2. Each oval is labeled by a region name (r i ), a mode name (Mk ), a clock interval ([u; v )), and an optional parametric condition ( : : :). A clock interval corresponds to the valuation of clock x in the system PTA description (Fig. 1). For ease of illustration, a parametric condition is given at the top of a sub-graph, instead of repeating it in each region of the sub-graph. Details of the iterations in our proposed PSynth() method (Table 4) are as follows.. . Initialization: In Step (2), regions satisfying are included in initial fix-point, z0 = fr1 ; r2 ; : : : ; r9 g..

(21) r47 M0 [0; 1). 6= 1 ^

(22) 3 r46 M0 [0; 1). =1^

(23) <3 r48 M0 [0; 1). r43 M4 [0; 1). r44 M0 [1; 2). r42 M0 [1; 2). r45 M0 [1; 1]. r39 M4 [1; 2). r40 M0 [2; 3). r38 M0 [2; 3). r41 M1 [0; 1). r35 M4 [2; 3). r36 M0 [3; 4). r34 M0 [3; 4). r37 M1 [1; 2). r31 M4 [3; 4). r32 M0 [4; 5). r29 M2 [3; 4). r30 M0 [4; 5). r33 M1 [2; 3). r24 M4 [4; 5). r25 M0 [5; 6). r20 M2 [4; 5). r21 M0 [5; 6). r28 M1 [3; 4). r16 M4 [5; 6). r26 M0 [6; 7). r13 M2 [5; 6). r22 M0 [6; 7). r19 M1 [4; 5). r4 M5 [5; 6). r14 M2 [6; 7). r23 M0 [7; 7]. r5 M5 [6; 7). r7 M5 [5; 6). r17 M4 [6; 7). r8 M5 [6; 7). r18 M4 [7; 7]. r27 M0 [7; 7]. r9. M5 [7; 7]. r1 M5 [5; 6). r10 M1 [5; 6). r15 M2 [7; 7]. r2 M5 [6; 7). r11 M1 [6; 7). r6. r3 M5 [7; 7]. r12 M1 [7; 7]. M5 [7; 7]. Figure 2: Pruned Parametric Region Graph for Example 1. L(r37 ) = ( = 1 ^

(24) < 3 ^ 5 7), L(r38 ) = ( 6= 1 ^

(25) 3 ^ 4 6), L(r39 ) = 5 7, L(r40 ) = L (r35 ).. . In Step (5), the next fix-point region space is computed as z6 = fr1 ; : : : ; r40 ; r41 ; : : : ; r44 g.. . . Iteration i = 6: In Step (4), new regions in z 6 are labelled with parametric conditions as follows L(r41 ) = ( = 1 ^

(26) < 3 ^ 6 8), L(r42 ) = ( 6= 1 ^

(27) 3 ^ 5 7), L(r43 ) = 6 8, L(r44 ) = L (r39 ). In Step (5), the next fix-point region space is computed as z7 = fr1 ; : : : ; r44 ; r45 ; : : : ; r47 g. Iteration i = 7: In Step (4), new regions in z 7 are labelled with parametric conditions as follows L(r45 ) = ( = 1 ^

(28) < 3 ^ 6 8), L(r46 ) = ( 6= 1 ^

(29) 3 ^ 6 8),. L(r47 ) = L (r43 ). . In Step (5), the next fix-point region space is computed as z8 = fr1 ; : : : ; r47 ; r48 g. Iteration i = 8: In Step (4), new regions in z 8 are labelled with parametric conditions as follows L (r48 ) = ( = 1 ^

(30) < 3 ^ 7 9). In Step (5), the next fix-point region space is computed as z9 = fr1 ; : : : ; r48 g, which is the same as z8. Hence, the loop terminates in Step (6). Step (7): 46. . The set of initial regions is. fr ; r ; r g. 48. R0 =. 47. Step (8): The general parametric condition is obtained as:. VH; = L (r46 ) _ L (r48 ) _ L (r47 ) = ( = 6 1 ^

(31) 3 ^ 6 8)_ ( = 1 ^

(32) < 3 ^ 7 9)_ (6 8). . (4). Step (9): The system synthesized is illustrated in Fig. 3..

(33) x=0. [3] R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183 – 235, 1994.. M0 =1^ x = 1 6= 1 ^ x := 0 x>3. x7. ^x7. M1. M2. M4.

(34) 3^.

(35) <3^ 5x7. 5x7. x := 0. [4] E. Asarin, O. Maler, and A. Pneuli. Symbolic controller synthesis for discrete and timed systems. In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, volume 999, pages 1 – 20. Lecture Notes in Computer Science, Springer Verlag, 1995.. 5x7. M5. 5x7. Figure 3: Synthesized PTA SC for Example 1. . Step (10): (VH; ; SC ) is the final output result.. 5 Conclusion An embedded real-time system synthesis problem was extended to include static parameters in system descriptions and quantitative parameters in specifications. The parametric embedded real-time system (PERTS) synthesis problem was presented and solved. A PERTS synthesis algorithm based on iterative system synthesis was proposed to solve the problem. The completeness and soundness of the algorithm were validated analytically. An example experiment was conducted to show the feasibility of our PERTS synthesis algorithm. Using our approach, system engineers can now take system parameters into consideration while designing embedded real-time systems. The formal approach also allows correct verified designs.. References [1] K. Altisen, G. Gobler, A. Pneuli, J. Sifakis, S. Tripakis, and S. Yovine. A framework for scheduler synthesis. In RealTime System Symposium (RTSS’99). IEEE Computer Society Press, 1999. [2] R. Alur, C. Courcoubetis, N. Halbwachs, and D. Dill. Modeling checking for real-time systems. In Proc. IEEE Logics in Computer Science, 1990.. [5] E. Asarin, O. Maler, A. Pneuli, and J. Sifakis. Controller synthesis for timed automata. In Proc. System Structure and Control. IFAC, Elsevier, July 1998. [6] V. Carchiolo, M. Malgeri, and G. Mangioni. Hardware software synthesis of formal specifications in codesign of embedded systems. ACM Transactions on Design Automation of Electronic Systems, 5(3):399–432, July 2000. [7] J.-M. Fu, T.-Y. Lee, P.-A. Hsiung, and S.-J. Chen. Hardwaresoftware timing coverification of distributed embedded systems. IEICE Trans. on Information and Systems, E83D(9):1731–1740, September 2000. [8] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proc. IEEE Logics in Computer Science, 1992. [9] P.-A. Hsiung. Embedded software verification in hardwaresoftware codesign. Journal of Systems Architecture — the Euromicro Journal, 46(15):1435–1450, November 2000. [10] P.-A. Hsiung. Hardware-software timing coverification of concurrent embedded real-time systems. IEE Proceedings on Computers and Digital Techniques, 147(2):81–90, March 2000. [11] P.-A. Hsiung. POSE: A parallel object-oriented synthesis environment. ACM Transactions on Design Automation of Electronic Systems, 6(1):to appear, January 2001. [12] O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In E.W. Mayr and C. Puech, editors, 12th Annual Symposium on Theoretical Aspects of Computer Science (STACS’95), volume 900, pages 229 – 242. Lecture Notes in Computer Science, Springer Verlag, March 1995. [13] P.J. Ramadge and W.M. Wonham. Supervisory control of a class of discrete event processes. SIAM Journal of Control and Optimization, 25:206 – 230, 1987. [14] P.J. Ramadge and W.M. Wonham. The control of discrete event systems. Proceedings of the IEEE, 77:81 – 98, 1989. [15] F. Wang and P.-A. Hsiung. Parametric analysis of computer systems. In Michael Johnson, editor, International Conference on Algebraic Methodology and Software Technology (AMAST’97), volume 1349, pages 539 – 553. Lecture Notes in Computer Science, Springer Verlag, December 1997. [16] H. Wong-Toi. The synthesis of controllers for linear hybrid automata. In Procs. CDC’97, 1997. [17] H. Wong-Toi and G. Hoffman. The control of dense real-time discrete event systems. Technical Report STAN-CS-92-1411, Stanford University, 1992..

(36)