Monitoring time property in time-sensitive LSC

Haiyang Xu,YiZhuang,and Jingjing Gu

1.Schoolof Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China; 2.Schoolof Science and Information,Qingdao Agricultural University,Qingdao 266109,China

Monitoring time property in time-sensitive LSC

Haiyang Xu1,2,YiZhuang1,*,and Jingjing Gu1

1.Schoolof Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China; 2.Schoolof Science and Information,Qingdao Agricultural University,Qingdao 266109,China

In order to accurately describe the software requirements and automatically extract property formulas,the time property of the live sequence chart(LSC)is focused.For the timesensitive LSC(TLSC),the formalsyntax and semantic are defined by introducing the formaldefinitions ofclock and timing constraints. The main function of the TLSC is to extract the temporal logic formula,so basic rules and combination rules are proposed to translate the TLSC into the universalfragmentofcomputation tree logic(CTL)formula.To improve the efficiency of model check, transitivity is also used to optimize the formula.The optimization method could reduce the size of the formula under the condition ofequivalence.Finally,a case study is introduced to illustrate how to establish the TLSC of requirements.In terms of the proposed transformation rules,the time property formula is extracted from the TLSC,and the design model is assured which is consistent with the property formula.The results show that the method with respect to the automatic extraction of the logic formula from the TLSC can efficiently monitorthe time property ofsoftware systems.

live sequence chart(LSC),timing constraint,temporal logic,transformation rule.

1.Introduction

In the process of system modeling and simulation,itis importantto accurately acquire the specification of a system, and makes it correct.Our motivation is to formally transform the specification and make what you wrote capture whatyou meant.Scenario-based language can graphically describe the software requirements,and can be used to verify the property of the design model.Live sequence chart (LSC)is one of the scenario-based modeling and specification languages,and it can be used at the stages of software design and developmentprocess.Atthe design stage, the LSC can be used to verify the properties of communication protocol,and assure the correctness of protocol behavior.At the development stage,the LSC can provide a specification for implementations that need to be verified[1].From the view of the property role,the LSC can describe the observe events among the system processes. While the LSC still adopts the timer and time interval in a message sequence chart(MSC),its application would be limited in the description ofcharacters and behaviorofthe realtime software system[2].

Model check can be used to verify whether a software modelsatisfies a given property ornot.There are two kinds of practicalmodelcheck categories.One is to translate requirementspecification of a software system into a set of temporal logic formulas,the other is to use an automaton to express the requirementspecification[3,4].Mostof the existing researches focus on translating LSC into automaton,or translating LSC into time B¨uchi automaton.There are few researches on translating LSC into temporallogic, and now no research on the transformation from the timesensitive LSC(TLSC)into temporallogic.

In the scenario-based software engineering,temporal logic is widely used to describe the software requirements [5,6],and model check is used to verify the consistency between the software modeland requirementspecification [7,8].While as the complexity of the logic structure,it is impracticalto require developers to directly use the temporallogic formula to signify the requirementspecification of a software system,it hinders formalverification in industrialapplications.Many researchers suggestusing the LSC to denote requirementspecification of the software system and extracting property formulas that need to be verified from the scenario-based language.However,the transformation rules from the LSC to temporal logic are nonstandard,and the software developers are differentin software requirementunderstanding,so the temporallogic formulas extracted from the LSC are different.Mostresearchers focus on the safety property and the liveness property,they rarely research on the time property of software behavior.

Forefficiently describing the properties and behaviorof the real time software,and automatically translating requirementspecification into logic formulas,we start from the existing scenario-based language,and focus on the definition and description of the time property in the scenario-based language.We present the TLSC to denote the requirements of the realtime software,which is the basis of translating requirement specification into temporal logic formulas.

We focus on the time property of the LSC,and introduce the formal definitions of clock and timing constraints.Based on the LSC,we propose the TLSC,and formally define its syntax and semantics.For eliminating the difference in extracting the property formula between developers and establishing the standard transformation rules,we presentthe basic transformation rules from TLSC to temporal logic formulas and the complex rules,which use logicalconnectors to compose the basic rules and combine path quantifier with basic rules.As the transfer efficiency from TLSC to temporallogic affects the complexity of verification work,we use transitivity to redefine the order property for optimizing formulas,and the improved method could reduce the size offormulas underthe formulas equivalence.

The remainder of the paper is organized as follow.Section 2 introduces some background on the LSC.The formal syntax and semantics of the TLSC are given in Section 3. In Section 4,we presentthe basic transformation rules and the combination rules.The result formula is further optimized in Section 5.Section 6 gives a case study to illustrate how to use the TLSC to describe the message sequence, and how to generate temporallogic formulas.Concluding remarks are given in Section 7.

2.Preliminaries

MSC has been standardized by the International Telecommunication Union(ITU)as the standard language and specification in the telecommunication behavior of real time systems,and ithas widespread in the developmentof industry software[9].While the weak partialorder semantics of the MSC makes it unable to describe some behavioral requirements[10],the MSC cannot precisely distinguish requirement and executable specification[11–13]. The faultof the MSC limits its expression ability.

Based on the extension ofthe ITUstandard forthe MSC, Damm and Harelproposed an LSC for scenarios[11].The LSC can model scenario-based software behavior in the form of a sequence diagram,and it is suitable to express the communication between processes[14].There is a universal mode and an existential mode in the LSC through adding liveness to the chart,so LSC can specify mandatory behavior and provisionalbehavior of a system.In the universalchart,allruns ofthe system satisfy the given scenario.While using the existentialchartto specify,the scenario can be satisfied by atleastone run ofthe system.Fig. 1 shows a universalchartof the LSC.An existential chart can represent the provisional scenario,and it is an inadequacy description for requirements.The existential chart is suitable for the early stage of software lifecycle.After gathering more software information,we can refine the existential chart to the universalchart[15].The messages of the LSC are divided into pre-chartand main-chart,both of which respectively denote the activation condition and the response eventof the scenario.In the universalchart,once the message in pre-chartis sent,itwillforce the message in main-chartto occur.While in the existentialchart,itwould notguarantee the message of main-chartto occur.

Fig.1 Universal chart of LSC

Hot and cold temperatures are introduced into LSC for chartelements,such as location,message and condition,to indicate thatchartelements must or may occur.As shown in Fig.1,LSC provisional behavior is represented by the dashed line,mandatory behavioris represented by the solid line.The pre-chart of the universal chart is specified by the dashed hexagon,the main-chartis drawn with the solid rectangle.The synchronous message is depicted by a solid arrow,while the asynchronous message is depicted by a dashed one.The two messages indicate thatthe communication between two instances must or may complete.The mandatory condition is denoted by the solid line hexagon, and the provisionalcondition is denoted by the dashed line hexagon.In Fig.1,Cond1denotes the mandatory condition,and it associates with I3and I4.When I3and I4satisfy Cond1atthe same time,I3willsend the synchronous message m4to I4.Cond2denotes the provisional condition,if I2satisfies the condition,I2will send the asynchronous message m5to I3.

The LSC extends the traditional MSC with mandatory behavior and forbidden behavior,and itcould specify scenario-based behavior specification of the reactive system in a more precise manner[16–18].The LSC has been successfully used in practicalhardware and software verification,such as the air traffic controlsystem[19]and therailway traffic management system[20].While the LSC still utilizes the timing constraint notations in the MSC, such as timer and time interval,doing this restricts the application of the LSC.

3.Syntax and semantics of TLSC

Compared with the MSC,the LSCnotonly remains advantages,such as visualization and understanding,butalso has the stronger expression ability which is similar to temporal logic[21].While the weakness of the LSC in the time property causes the addition of the expression of time for the LSC,which makes it equalto temporallogic formulas in the expression[22,23].To be more suitable for specifying the behavior and property of real time software,we extend LSC with formal clock and timing constraints to denote the time eventand time delay.Firstly we define the formalsyntax of TLSC,and then give the semantics of the universalchartin TLSC based on trace.

3.1 Formalsyntax of TLSC

Aimming to add the formal timing constraints for LSC [24],we firstly introduce some definitions abouttime,such as clock constraintand clock interpretation.

Definition 1(clock constraint)For a set C of clock variables,Φ(C)is a set of clock constraint?on C.And the clock constraint?is defined by

where x∈C is a clock variable,and c is a constantin Q+(Q+is the setofnonnegative integer).

Definition 2(clock interpretation)For a set C of clock variables,v is a clock interpretation for C.It is a mapping from C to R+and is defined by v:C→R+. Where v assigns a positive realvalue to each clock x,and x is a clock variable.

Clock constraints denote the time condition that should be satisfied when the eventoccurs.Aclock interpretation v could satisfy a clock constraint(denoted by v|=?)if and only if the value of?is true for the given value v.

Let the notation[?]={v|v|=?}denote the set of clock interpretation v that satisfies the clock constraint?. Forthe precursortime setand succeed time setofthe clock constraint?,we respectively use the notations pre(?)= {v|v＜min([?])}and succ(?)={v|v＞max([?])}to describe the clock values which occurbefore and after the clock constraint?[25].

Definition 3(TLSC)A TLSC is a tuple TLSC=〈I,Loc,E,C,δ,Mode,inv,μ〉,where

I is a setof instances in TLSC;

Loc is a setof locations in TLSC;

E is a set of events in TLSC,events are grouped into two sets:condition(Con)and message(Msg),thatis,E= Con∪Msg;

C is a finite setof clock variables;

δ:E→Loc is an eventmapping function,itmaps each eventto a location;

Mode:E→{cold,hot}is a behavior mapping function,itdenotes an eventis provisionalor mandatory;

inv:Loc→Φ(C)is a timing constraint function,it assigns timing constraints for each location〈i,l〉and the timing constraint inv(l)is the invariantofthe location;

μ:E→Φ(C)is a time interval function,it defines the time intervalof events,which denote the minimum and maximum time delay when an eventoccurs.

To more clearly understand the formal syntax of the TLSC,we give an example to depictthe timing constraints in the TLSC,as shown in Fig.2.When the instance I1is in the location〈I1,1〉and satisfies the invariant?,then I1will send the synchronization message m to I2.The message m should be sentand received within the time interval constraint[t1,t2]of the clock x,and the clock y is reset to 0.

Fig.2 Timing constraint in TLSC

3.2 Semantic of TLSC

In the section,we give the trace-based formalsemantic of the universalchartin the TLSC.

We use the symbol tl to denote a universal chart of TLSC,and use the set I={i1,i2,...,in}to denote all instances in tl.An instance may be a process,an object, or a component,etc.Each instance has an instance line, and we stilluse the same symbol I to denote the instance line.The finite locations are marked with numbers in instance lines by top-down.For the instance line i and the chart tl,the set of locations is given by dom(tl,i)= {l0(i),l1(i),...,lmax(i)}.Thus,we define a finite set of locations Loc={〈i,l〉|i∈I∧l∈dom(tl,i)}to representallthe locations in the chart tl.

In terms of Definition 3,there are two kinds ofevents in the chart tl,so E=Con∪Msg.

Definition 4The event E in one location l of the instance I is defined by

E:=[Con|ε],Msg|ε

Con:=[hot|cold],Boolexp

Msg:=[?|ε],＜[hot|cold],〈i,l〉,m,[?|ε],〈i?,l?〉＞

We regard the condition and message appearing in location as an event.When the condition Con satisfies theBoolean expression Boolexp,the system will execute the following event.The message is restrained by the sender and the timing constraint.The temperature values hot and cold indicate the message must or may occur,that is a synchronous message or an asynchronous message.The symbol〈i,l〉represents the senderof the message,and the sender also may be restrained by time.Once the sender satisfies the timing constraints,itwillsend the message m, which occurs during the minimum and maximum time delay.The symbol〈i?,l?〉represents the receiver of the message.

Definition 5CUT is the set of locations of all the instances in TLSC.And itis defined by CUT={cut|cut= (＜i1,l1＞,...,＜in,ln＞)∧i∈I∧l∈dom(tl,i)}, where cut is a mapping of current locations of all the instances in TLSC,and denotes a state ofsystem runs.If cut, cut?∈CUT,and cut=(＜i1,l1＞,...,＜in,ln＞),

Then cut?is a successor of the location＜j,lj＞of cut denoted by cut?=succ(cut,＜i,li＞).

The definition of CUT considers not only the current locations of instances,but also the timing constraint?in locations.

Definition 6The symbolδis a message function of the location〈i,li〉and its mapping relationship is defined by

In terms of the message functionδ,we can define the partialorderrelation between messages by?.

If the messages are in the same instance line,there is

If the messages are in differentinstance lines,there is

We denote the immediate successor of the message m by succ(m)={n|m?n∧n/=ε}.

Definition 7(order property)Given two messages ei=δ(i,li)and ej=δ(j,lj),if messages eiand ejsatisfy the partialorder ei?ej,then the orderproperty is

which denotes that the message ejwill not occur until eioccurs.

If messages eiand ejsatisfy the partial order ei?ejand ej=succ(ei),then the order property is

which denotes that the message ejwill occur next to ei, when eioccurs.

Definition 8(execution trace)Let a CUT sequence r=(cut0,v0),(cut1,v1),...,(cutk,vk)be a run of TLSC.Where cutidenotes a mapping ofcurrentlocations of all the instances in TLSC,and videnotes the clock interpretation of the current state.cut0is the starting point and clock interpretation v0=0,and cutkis the terminal point.(cuti,vi)=succ((cuti?1,vi?1),〈i,li〉)(i= 0,1,...,k?1).The setofallruns is denoted by the symbol Runs.We use rk={r|?r∈Runs∧|r|=k} to denote the subpath of the run r with k path,and use Path(cuti,vi)={r|?r∈Runs∧cut0=cuti}to denote a path of a run starting at(ci,vi).An execution trace is the trace ofa CUT sequence,and is denoted byπ=trace(r)

Thatis,π=π0,π1,...,πk?1denotes the events thattrigger the state transition,and

In terms of the execution trace,we define the trace-based language of the TLSC tl to be

The language L of the TLSC consists of the eventchain thattriggers the state transition.The problem thatthe software modelwhether satisfies the requirementspecification or not,can be reduced to the inclusion of language.

Since both pre-chartand main-chartcan be represented as a chain of events,they are the basic charts of an LSC. An LSC can be represented by a pre-chartand a fullchart, where the full chart is the concatenation of the pre-chart and the main-chart[5].The trace languages ofthe pre-chart and fullchartcan be defined byThe eventchain ofthe fullchartlanguage composes of the events with Cartesian product in the run of the pre-chart and main-chart.

4.Transformation of TLSC into temporal logic formula

As linear temporal logic(LTL)formulas cannot express the property in some pathes,the existentialchartcan be refined to a universalchart[15,26].We focus on the method extracting computation tree logic(CTL)formulas from the TLSC universalchart[27].A CTL formula can be written in the form of negation normal form(NNF),so each formula can be translated into an equivalentformula in NNF [28,29],thus all kinds of operators in formulas can be reduced.Based on the above analysis,we only use the formulas in NNF.ACTL is one subset of CTL formulas,and there is only the path quantifier A to express the branch of states,so the temporal operators in logic formulas are restricted to{AX,AF,AG,AU,AR}.We further use the sub logic ACTL of the CTL.In the process of translating the universal chart of the TLSC into temporal logic,we only discuss how to translate itinto ACTL formulas.

If the event defined in the pre-chartoccurs in the given order,the sequence of events defined in the main-chart mustoccur in the given order[5].Thatis,a universalchart ofthe TLSCcan be used to specify requirementsin temporal formula form.In terms of the trace-based semantic of the TLSC,we will translate the scenario-based TLSC requirementinto an ACTL formula.The transformation rule setis composed of two rules:the basic rules and the combination rules.

4.1 Basic rules

In the basic rules,we do notconsiderthe effects ofthe path quantifier.The transformation rules are to translate a TLSC message into a simple ACTL formula.Firstly,we give the formaldefinition of the CTL formula:

PQ is a set of the path quantifier,which denotes the branch of the states.TO is a set of temporal operator, which denotes the order relationship between two states. AP is a setof atomic proposition.

Rule 1(single message transformation rule)The name of the message is mapped to an atomic proposition. In terms of the behavior mapping function,we decide the temporaloperator and generate a unary temporalformula, which nesta binary temporalformula.The temporaloperator of the binary temporalformula is U,the first element is the negation of atomic proposition,the second element is atomic proposition.If the sender of the message is limited by the timing constraint,then the constraint is mapped to the operator U.The delay intervalconstraintof the message is mapped to a formula thatconjuncts with the atomic proposition.The formaldescription is as follows.

mapSingleMsgToCTL:SingleMsg→CTL

Fig.3 Basic transformation rules

Fig.3 shows the basic transformation rules which translate a single message into an ACTL formula.Fig.3(a) denotes that message and location are not limited by the timing constraint,and the temperature of the message is hot,so it is directly translated into an ACTL formula G((?m)Um).The hot temperature denotes the message must occur,thus we adopt the temporaloperator G to denote that atomic proposition always occurs.Fig.3(b)denotes that the location of the message sender would satisfy the timing constraint?,and then itcan be sent.Hence the ACTL formula is G((?m)U?m).In Fig.3(c),except the constraint on location,the message also needs to sa-tisfy the delay constraintΦ,so the TLSC is translated into G((?m)U?(m∧Φ).

Fig.3(d)shows an ACTL formula translated from an asynchronous message.The temperature of the message is cold,and the sender is notlimited by the timing constraint, so the ACTL formula is F((?m)Um).The cold temperature denotes that the message maybe occur,so we adopt the temporal operator F to show that the atomic proposition will occur in the future.Fig.3(e)shows the timing constraint?on the sender location,so the ACTL formula is F((?m)U?m).Fig.3(f)also shows the delay constraint Φon the message thatshould be satisfied,so the translated resultis F((?m)U?(m∧Φ).

4.2 Combination rules

We have defined the basic transformation rules,but they can only refer to a single message and they cannot deal with the situation of multiple messages.Now we present the combination rules,which are divided into two kinds. One is to use logicalconnective to combine the basic transformation rules,the other is to combine the path quantifier with transformation rules.

Lemma 1(proposition composability)Let TLSC=＜I,Loc,E,C,δ,Mode,inv,μ＞be a TLSCmodel,cutiis a state of the run r of the TLSC,φandψare ACTL formulas,then

(i)if TLSC,cuti|=φand TLSC,cuti|=ψ,then TLSC,cuti|=φ∧ψ,T LSC,cuti|=φ∨ψ;

(ii)if TLSC,cuti|=φand TLSC,cuti|=ψ,then TLSC,cuti|=φ→ψ.

In the universalchart,allruns satisfy the given scenario. We give the combination rules,which are used to combine the ACTL formula corresponding with message in differentstates of runs.

Rule 2(combination rule)Forthe two messages in the run r of the TLSC,they respectively correspond to a temporal logic formula.If the two messages are in the same sub chart,the relationship between formulas is logicalconjunction.If the two messages are in different sub charts, the relationship is logicalimplication.The mapping rule is described as follows:

combineMsg ToCTL:Msg→CTL

?m1,m2:Msg·combineMsg ToCTL(m1,m2)=

{ctl,ctl1,ctl2:CTL|ctl1=mapSingleMsg ToCTL (m1)∧ctl1=mapSingleMsg ToCTL(m2)

if(type(m1)==type(m2)∧m2==succ(m1)) then ctl=ctl1∧ctl2∧φm1,m2

if(type(m1)!=type(m2)∧type(m1)== pre-chart)then ctl=ctl1→ctl2}.

The function type returns the type ofsub charts to which message belongs.

Fig.4 shows an example of combination formulas.In Fig.4(a),the messages m and n satisfy n=succ(m).After the message m occurs,ifthe location of I2satisfies the timing constraint?,then the message n occurs.And according to the order property defined in Definition 7,the combination formula is

In Fig.4(b),the message m occurs in the pre-chart.Satisfying the timing constraint?on the sender location,the message n occurs in the main-chart and also satisfies the delay constraintΦ.The combination formula is

Fig.4 Combination formula oftwo messages

If messages m and n in Fig.4(a)are all applied in the form of Fig.3(c),then the combined result is G((?m)∧(?n))U?1(m∧Φ1)∧(X?2(n∧Φ2)).As the message is the trace of the CUT sequence,in terms ofthe trace-based language,the ACTL formula of the universal chart is defined by

Let Lpchand Lfchrespectively denote the trace-based language of the pre-chart and full chart,andφπdenote the ACTL formula of the sub chartwhereπis the trace of the CUT sequence.

Lemma 2(path quantifier composability)

Let TLSC=＜I,Loc,E,C,δ,Mode,inv,μ＞be a TLSC model,r is a run of TLSC,φis an ACTL formula, then

The universalchartis used to denote the mandatory scenario.If the eventin the pre-chart is activated,there must be a response event in the main chart.Thus,the general ACTL formula of the universal chart is further described as follows:

For the ACTL formulaφπofthe TLSC sub chart,ifthe temperature of the message is hot,then the ACTL formula is AGφ,which denotes thatφis true in all the achieved states of runs.If the temperature of the message is cold, then the ACTL formula is EFφ,and it denotes that there exists a run in whichφis true.

Theorem 1Let T LSC=＜I,Loc,E,C,δ,Mode, inv,μ＞be a TLSC model,r is a run of the TLSC,rkis a sub run with the length k,φis an ACTL formula,then cut|=φiff cutk|=φ.

ProofUsing induction

Ifφ=AP,then T LSC,rk|=AP means AP∈L(rk), and in terms of the semantic of CTL,we have T LSC,r|= ~φ.

Ifφ=γ∧ψ,then in terms of the Lemma 1, TLSC,rk|=γand T LSC,rk|=ψ.And in terms of the induction assumption,TLSC,r|=γand TLSC,r|=ψ, thatis TLSC,r|=γ∧ψ.

Ifφ=γ∨ψ,then in terms of Lemma 1,TLSC,rk|=γ or TLSC,rk|=ψ.And in terms of the induction assumption,T LSC,r|=γor TLSC,r|=ψ,thatis TLSC,r|= γ∨ψ.

For the temporaloperators,we consider in case of AG, φ=AGψ.

In terms of Lemma 2,for?i?k,and TLSC,rki|=ψ, we have T LSC,cuti|=ψ.

For?i＞k,suppose that rk+1is a sub run of TLSCwith the length k+1,and rkis a path prefix of rk+1.Then there is a Path(cut0,v0)such that rk+1∈Path(cut0,v0)∧rk∈Path(cut0,v0).Then rk+1=rk∧cutk+1or rk+1= rk∨cutk+1.In terms ofthe induction assumption,TLSC, rk+1|=ψ.And in terms of Lemma 2,TLSC,r|=AGψ. ? Theorem 1 shows thatthe run of the TLSC satisfies the bounded semantic of the ACTL.That is,if the property holdsin bounded semantic,then itmusthold in CTL.Thus, the temporal logic formula extracting from the specification can be used to bounded modelchecking[30].

5.Optimized formula

In the practicalapplication,the major limitation is thatthe length ofthe temporallogic formula directly influences the verification efficiency.Even for the moderate sized LSC, its translated result grows large and it is also against the verification of model checking tools.If there are lots of concurrentoperations,itwillmake a higher costof formal verification[31].To improve the formalverification of the LSC,Klose et al.propose bonded and time bounded subclasses of the LSC to quickly check whetherthe modelsatisfies the requirements or not[2].Although this method is faster than LTL modelchecking,butless is powerful.In terms of the transformation from LSC to temporal logic, Kumar etal.presenta rigor method which uses logic minimization over the unitl(U)operator to improve the size of the formula,and reduce the verification time and state space[1].The size of the reduction formula is at most quadratic size of the chart.Based on the method,we make use of transitivity to redefine the time order property,and optimize the order formula transformed from the TLSC to reduce the size of the formula.

Let p∈Msgp,m∈Msgmand e∈Msg respectively denote the messages in pre-chart,main-chartand fullchart. In terms of the transformation rules,we can translate the TLSC into the ACTL formula.We define the order property in Definition 7,and if the messages eiand ejsatisfy the partial relation ei/?ej,then the uniqueness property can be represented byχei,ej=(?ei∧?ej)U(ei∧X((?ei∧?ej)Uei))[1].This means that message eioccurs twice before ej.The ACTL formula can be defined by

The above formula only contains the order property and the uniqueness property between messages,not considers the timing constraints.In addition,the sheersize ofthe formula effects the properties verification.Based on the formula,we add the timing constraints to optimize the formula.

Lemma 3For a given execution traceπ=π0,π1,... and three messages eu,ev,et,and ev=succ(eu),et= succ(ev)

Lemma 3 shows thatthe order properties between messages satisfy transitivity,and the relationship between timing constraints is logicalconjunction.The lemma reduces the order properties between two messages of a message sequence to the orderproperties between the head message and other messages,and can simplify the ACTL formula.

Lemma 4For a message set N and a message ej,if?ei∈N and N={e|e∈succ(ej)},ej?ei,then the execution traceπ=π0,π1,...satisfies

Lemma 4 shows if a message satisfies different timing constraints,then it would have several successors.Thus those successors would notoccuruntilitsatisfies the minimum timing constraint.

According to Lemma 4,the order property defined in Definition 7 can be redefined by

Forthe optimization ofthe uniquenessproperty,we only ought to establish the uniqueness formulas between each message of the sub chart and the final message[32],and we do not need to establish the uniqueness formulas between any two messages.

According to Lemma 3,Lemma 4 and uniqueness optimized formulas[1],the ACTL formula can be optimized as pj=Maxp(ij)denotes the final message in instance ijof the pre-chart.mj=Maxm(ij)denotes the final message in instance ijof the main-chart.Finv+umjdenotes that the message mjwould occur in the end,whose timing constraintis the sum of timing constraintin the sender location and the time delay when the eventoccurs.

Theorem 2Letφbe an ACTL formula,φ?be an optimized ACTL formula,ψbe an LTL formula.Then the execution traceπ=π0,π1,...satisfies

(i)TLSC,π|=φiff TLSC,π|=φ?; (ii)φ??ψif fψcan be denoted asφ.

ProofFor(i),by Lemma 3,Lemma 4 and uniqueness optimized formulas[1],itcan be proved.

For(ii),according to the conclusion proposed by Clarke and Draghilescu[33]:a CTL formula is equivalent to an LTL formula,if and only if after removing the path quantifier,the CTL formula is also equivalent.Furthermore,Boja′nczyk[34]presented an algorithm to distinguish whetheran LTL formula can be denoted as an ACTL formula or not.?

6.Case study

We illustrate the use of the TLSC in the contextof an embedded software froma controlsystem.The aim is notonly to demonstrate the applicability of the TLSC to monitor the property of the software system,but also to translate the TLSC into ACTL formulas.We can achieve the liveness formula,safety formula and real time formula,then we analyze and verify the realtime formula.

6.1 TLSC modeling

The controlsoftware consists of sensor,database(DB),information processing(IP),equipmentcontrol(EC)and execution unit(EU).The DB module is used to store alldata in the system.The data are acquired by the sensor module, and then send to the IP module.The IP module is used to process the data,and send the result data to EC the module.The EC module could parse the result data,achieve the equipment control command,and send the command to EU the module.The EU module is used to execute the command and feed back the execution result.

The real time requirements of the software system are thatthe onetime ofdata acquisition is no more than 1 s,and the delay time of data transmission is less than 2 s.The IP module requires thateach iteration processing time should be no more than 1 s.The ECmodule sends the command to the EU module within 2 s,and requires the feedback time from the EU module to be less than 5 s.Fig.5 shows the property requirements of the software system in terms of the TLSC.

Fig.5 Requirements in TLSC

6.2 Generation of temporalformula

As the run of the TLSC is a CUT sequence,the property requirements of the software system can be achieved by the state transitions in the CUT sequence.In terms of the TLSC of the controlsoftware,we can getthe property which need to be verified,and require the design model to be consistent with requirement specification.In Fig.5, when the sensor module satisfies the timing constraint t＜1,the software system executes the message send, sends the acquisition data to the IP module and requires the send timing constraint x＜2.IP module receives the data and executesthe message process,then sends the processed data to EC and requires the processing timing constraint y＜1,the send time is resetto 0.ECmodule parsesthe data and executes the message command,then sends the command to EUand requiresthe send timing constraint u＜2,the iteration time of process is resetto 0.In terms ofthe proposed transformation rules,we can getthe ACTL formula:

In terms of the optimized formula,the above ACTL formula can be optimized as follows:

The formula describes the liveness property of the software system and requires that the software model should hold the property specification.Thatis,after the sensoracquired the data,EC module needs to send a command data within 4 s.

In the Fig.5,sensor,IP,EC and EU respectively access the DBmodule underdifferenttiming constraints.Thus we can getthe ACTL formula of the safety property:

That is,at any time no more than one module can access the database DB.

Now we extract the ACTL formula from the whole TLSC.After the system sends the message start to the sensor,all the modules start work.And after one module sends its message to the other module,sensor,IP, EC,EU all send the message store.As the message store closely keeps up with the other message,it has no extra timing constraints.For reducing the complexity of the formula,we assume that the message store occurs with the othermessage atthe same time,so thatwe ignore the effect of the message store for the formula.The ACTL formula is as follows:

From the above formula,we can deduce the real time property formula by

AG denotes the property must be satisfied,and AF denotes the property will occur in the future.The real time formula shows that the software system starts sensor module,and the totaltime of receiving the feedback message is no more than 9 s.

6.3 Result analysis

For the real time property formula,we use the probabilistic symbolic model checker(PRISM)[35]to verify the property ofthe software design model.There are two property specification languages probabilistic CTL(PCTL)and LTL in PRISM,where the main difference between PCTL and CTL lies in the path quantifier.There are two path quantifiers A and E in CTL,while PCTL only uses the general path quantifier,to assign arbitrary probability to the path formula.Thus,the path quantifier in CTL can be denoted by the equivalent PCTL formula[36].For the furtherstudying probability in TLSC,we use PCTL in PRISM to describe the realtime property formula.

From the real time property formula in the above section,after the software system starts the sensor,all the modules start run within 1 s,and the system receives the feedback within 9 s.We use the reward-based property to denote the formula AFt＜9f eedback:

For the given state of the software model,the formula can calculate the expected time values within 9 s reword.

We extract specification formula from the TLSC of the control software,and use modeling and analysis of real time and embedded(MARTE)systems to establish the state transition model of the control software.Then we use PRISM language to respectively describe the specification and the model.We can verify that the above PCTL formula is true.The software design model is consistent with the real time property formula extracted from TLSC. From Table 1,the initialtransformation formula can reflect the real time requirements of the control software,but it takes longertime in modelverification.The size of the improving formula is smaller than the initialformula,and itsverification time is only 25%of the originalformula.The availability and efficiency have greatly increased than the originalformula.

Table 1 Verification time s

7.Conclusions

How to accurately achieve the software requirement property and precisely signify the temporallogic formula from requirementspecification are importantcontents in model check.Extracting temporal logic formula from the LSC can solve the fault in specification expression caused by human error.There are severalresearches on transforming the LSC into the temporallogic formula,but they mainly focus on the safety property and the liveness property,but no research focuses on the automatically extracting time property.

Based on the LSC,we introduce clock and timing constraints to describe the time-sensitive LSC,and give the formaldefinition of the TLSC and the trace-based semantic of the TLSC.For the transformation from the TLSC to ACTL,we consider the effect of the path quantifier, then study the transformation from the basic rules and the combination rules respectively.In the practical application,the main limitation of the translated ACTL formulas lies in the size.For reducing the formula size,we propose an optimization method for the translated formula,which can remarkable reduce the effect of the time property for the complexity of the formula.The case study shows that our method can availably extract ACTL formulas from the TLSC,meanwhile the optimized method can improve the verification time.Therefore,our method can be used to automatically extract specification from software requirements,and verify whether the design model is consistent with requirementspecification or not.

[1]R.Kumar,E.G.Mercer,A.Bunker.Improving translation of live sequence chartsto temporallogic.Electronic Notes in TheoreticalComputer Science,2009,250(1):137–152.

[2]J.Klose,T.Toben,B.Westphal,et al.Check it out:on the efficient formal verification of live sequence charts.Proc.of the 18th International Conference on Computer Aided Verification,2006:219–233.

[3]E.M.Clarke,E.A.Emerson.Design and synthesis of synchronization skeletons using branching time temporal logic. Lecture Notes in Computer Science,2008,5000:196–215.

[4]W.Chan,R.J.Anderson,P.Beame,et al.Model checking large software specifications.IEEE Trans.on Software Engineering,1998,24(7):498–520.

[5]D.Lo,S.Maoz.Scenario-based and value-based specification mining:bettertogether.Automated Software Engineering, 2012,19(4):423–458.

[6]S.Maoz.Polymorphic scenario-based specification models: semantics and applications.Software and Systems Modeling, 2012,11(3):327–345.

[7]J.Sun,J.S.Dong.Modelchecking live sequence charts.Proc. of the 10th IEEE International Conference on Engineering of Complex Computer Systems,2005:529–538.

[8]H.F.Guo,W.Zheng,M.Subramaniam.Consistency checking for LSC specifications.Proc.of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering,2009:119–126.

[9]A.Roychoudhury,A.Goel,B.Sengupta.Symbolic message sequence charts.ACM Trans.on Software Engineering and Methodology,2012,21(2):11–44.

[10]H.Dan,R.MHierons,S.Counsell.A framework forpathologies of message sequence charts.Information and Software Technology,2012,54(11):1283–1295.

[11]W.Damm,D.Harel.LSCs:breathing life into message sequence charts.FormalMethods in System Design,2001,19(1): 45–80.

[12]R.Marelly,D.Harel,H.Kugler.Multiple instances and symbolic variables in executable sequence charts.Proc.of the 17th Annals ACM Conference on Object-oriented Programming, Systems,Language and Applications,2002:83–100.

[13]D.Harel,I.Segall.Synthesis from scenario-based specifications.Journal ofComputer and System Sciences,2012,78(3): 970–980.

[14]M.Chai,B.H.Schlingloff.Monitoring systems with extended live sequence charts.Proc.of the 5th International Conference on Runtime Verification,2014:48–63.

[15]W.R.Li,Z.J.Wang,P.C.Zhang.Formalsemantics ofuniversalmodalsequence diagram.JournalofSoftware,2011,22(4): 659–675.(in Chinese)

[16]H.F.Guo,W.Zheng,M.Subramaniam.L2C2:logic-based LSC consistency checking.Proc.of the 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming,2009:183–194.

[17]H.F.Guo,M.Subramaniam.Model-based testgeneration using extended symbolic grammars.International Journal on Software Tools for Technology Transfer,2014,16(4):437–455.

[18]P.Combes,D.Harel,H.Kugler.Modeling and verification ofa telecommunication application using live sequence charts and the play-engine tool.Software and Systems Modeling,2008, 7(2):157–175.

[19]Y.Bontemps,P.Heymans,H.Kugler.Applying LSCs to the specification of an air traffic control system.Proc.of the 2nd International Workshop on Scenarios and State Machines: Models,Algorithms,and Tools,2003:1–7.

[20]J.Bohn,W.Damm,J.Klose,et al.Modeling and validating train system applications using statemate and live sequence charts.Proc.of the 6th Biennial World Conference on Integrated Design and Process Technology,2002:1–9.

[21]W.Damm,T.Toben,B.Westphal.On the expressive power of live sequence charts.Lecture Notes in Computer Science, 2007,4444:225–246.

[22]P.C.Zhang,W.R.Li,D.S.Wan,etal.Monitoring of probabilistic timed property sequence charts.Software:Practice and Experience,2011,41(7):841–866.

[23]B.Cohen,S.Maoz.Semantically configurable analysis of scenario-based specifications.Proc.of the 17th International Conference on Fundamental Approaches to Software Engineering,2014:185–199.

[24]W.R.Li,P.C.Zhang.On the semantics of scenario-based specification based on timed computationaltree logic.Proc.of the 22nd Australasian Conference on Software Engineering,2013:1–10.

[25]P.C.Zhang,B.X.Li,L.Grunske.Timed property sequence chart.Journal of Systems and Software,2010,83(3):371–390.

[26]L.Xu,W.Chen,Y.Y.Xu,et al.Improved bounded model checking for the universal fragment of CTL.Journal of Computer Science and Technology,2009,24(1):96–109.

[27]Y.T.Dai,H.K.Miao,J.Mei,etal.Property extraction based on LSC modelchecking.JournalofShanghaiUniversity(NaturalScience),2012,18(2):156–162.(in Chinese)

[28]W.H.Zhang.Bounded semantics of CTL and SAT-based verification.Proc.ofthe 11th International Conference on Formal Engineering Methods,2009:286–305.

[29]A.Zbrzezny.A new translation from ECTL*to SAT.Fundamenta Informaticae,2012,120(3):375–395.

[30]J.J.Yang,K.L.Su,X.Y.Luo,etal.Optimization ofbounded model checking.Journal of Software,2009,20(8):2005–2014.(in Chinese)

[31]T.Toben,B.Westphal.Concurrent LSC verification:on decomposition properties of partially ordered symbolic automata.Electronic Notes in Theoretical Computer Science, 2006,145:95–111.

[32]H.Kugler,D.Harel,A.Pnueli,et al.Temporal logic for scenario-based specifications.Proc.of the 11th International Conference on Tools and Algorithms for the Construction and Analysis ofSystems,2005:445–460.

[33]E.M.Clarke,I.A.Draghicescu.Expressibility results for linear-time and branching-time logics.Lecture Notes in Computer Science,1989,354:428–437.

[34]M.Boja′nczyk.The common fragment of ACTL and LTL. Proc.of the 11th International Conference on Foundations of Software Science and Computational Structures,2008:172–185.

[35]M.Kwiatkowska,G.Norman,D.Parker.PRISM 4.0:verification of probabilistic real-time systems.Proc.of the 23rd International Conference on Computer Aided Verification,2011: 585–591.

[36]H.Hansson,B.Jonsson.A logic for reasoning abouttime and reliability.Formal Aspects of Computing,1994,6(5):512–535.

Biographies

Haiyang Xuwas born in 1981.He received his B.S. degree in mathematics from the School of Mathematical Science,Shandong Normal University in 2003,and the M.S.degree in computer application technology from the School of Information Technology,Capital Normal University,in 2006.Since 2006,he has been a faculty member with School of Science and Information,Qingdao Agriculture University.He was as a lecturer since 2008.Currently he is pursuing his Ph.D.degree at Schoolof Computer Science and Technology,Nanjing University of Aeronautics and Astronautics.He is a member of China Computer Federation(CCF).His research interests include formalmethod,modeltransformation,and modelchecking.

E-mail:xhy@nuaa.edu.cn

Yi Zhuangwas born in 1955.She is currently a professor and Ph.D.supervisor of computer science in School of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics.Her research interests include distributed computation,information security,and trusted computing.

E-mail:zy16@nuaa.edu.cn

Jingjing Guwas born in 1983.She received her Ph.D.degree from School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics.Now she is an associate professorof School of Computer Science and Technology at Nanjing University of Aeronautics and Astronautics.Her main research fields are data mining and wireless sensornetwork.

E-mail:gujingjing@nuaa.edu.cn

10.1109/JSEE.2015.00093

Manuscript received June 25,2014.

*Corresponding author.

This work was supported by the National Natural Science Foundation of China(61202351),the China Postdoctoral Science Foundation (2011M500124),the Fundamental Research Funds for the Nanjing University ofAeronautics and Astronautics(NS2012133),and the Funding of Jiangsu Innovation Program for Graduate Education and the Fundamental Research Funds for the Central Universities(CXLX12 0161).