Software designers widely use UML Class Models to specify the static structure of object-oriented systems. Temporal properties of class models can be expressed using the TOCL, an extension of OCL with elements of a linear temporal logic. Speci cation and veri cation of temporal properties expressed in TOCL is non-trivial and no automated tools exist that aid such veri cation. Existing approaches rely on transforming the UML models to other languages that have automated analysis support. Such transformation is complex and can introduce errors. Towards this end, this paper proposes a framework for specifying and directly analyzing temporal properties expressed in TOCL. The framework was validated using two demonstration case studies and in both cases, the approach uncovered design faults.
UML Class Models are probably the most common speci cation diagrams used
in the software industry. Automated analysis of class models often uncovers
design problems in a timely manner and therefore saves time and e ort.
Specifying and analyzing temporal properties of class models is non-trivial due to
the following challenges. First, specifying temporal properties in formal
temporal logic notations, such as LTL and CTL, can be challenging [
This research proposal presents a framework that addresses the preceding challenges. In particular, the framework aims to provide the following results: (1) a class model analysis approach that is UML-oriented, (2) an object-oriented technique for specifying temporal properties, and (3) a development process with an automated tool. A successful development of such framework will yield results that can be utilized by MDE practitioners to develop reliable complex systems.
A number of model-checking-based techniques exist for specifying and analyzing
temporal properties in UML behavioral models, such as statemachines and
activity diagrams [2{10]. These techniques involve developing an exogenous
transformation process. Typically, the UML behavioral models are transformed to
languages that are supported by model checking tools. For example, the vUML [
Three main shortcomings are associated with these approaches. First, e ective
use of these model-checking techniques requires developers to have specialized
skills that are not UML-related. Second, the correctness of the analysis results
depends on the correctness of the transformation and whether it preserves the
semantics of the source UML models. Third, the results of the analysis performed
by the back-end analysis tool must be presented to developers in UML terms in
order to be examined, thus requiring another transformation process.
The existing structural anlaysis tools of UML/OCL such as USE [
The UML-based analysis approach
The research question that led to this approach is the following: Given a UML
design class model, and a temporal property, is there a scenario, which is supported
by the class model, that violates the property? A design class model speci es the
set of all possible states of a system and includes operations contracts to specify
the system behavior. A scenario is a sequence of state transition supported by
the class model. A temporal property is speci ed in TOCL, which is a temporal
logic extension of OCL [
Operation OCL Constraints context A::Aop():void pre:self.b→notEmpty() pre:self.A_att=false post:self.A_att=true context B::Bop():int pre:self.a.A_att =true
A -A_att : Boolean +Aop(in k : Boolean) -a 0. 1 -b 0. 1
B -B_att : Boolean +Bop() : int creates System specified in designer specifies B_att becomes true in next state in response to A_att being true in current state. --------------------------------context A inv: self.A_att= true implies next self.b.B_att=true
Snapshot Transition Model(STM) context Snapshot::getNext():Snapshot = self.nextT.nextS context Snapshot::futureClosure(sp : Set(Snapshot)) : Set(Snapshot)= if sp→includesAl (sp→col ect(sn:Snapshot | sn.getNext())→asSet()) then sp else futureClosure(sp→union (sp→col ect(t:Snapshot| t.getNext())→asSet()))endif context Snapshot::getPost(): Set(Snapshot) = self.futureClosure(Set{self.getNext()}) {-obredfoerreedS} 1 Before Aop
Snapshot 0.T1ransi{toio-rnndeexretTd} ---kAAPP:roBesot:o:AleAan OCL Constraints context Aop inv: APre.b→notEmpty() inv:APre.A_att =false inv:APost.A_att=true context Bop inv:BPre.a.A_att=true
a:A A_at :Boolean
b:B B_at :Boolean
Bop -b{oerfdoerereTd} 0. 1 -BPre : B -BPost : B 1 {o-rndeexrteSd} After specified in -ret : int context A inv: let CurrentSnapshot: Snapshot = self.getCurrentSnapshot() in let NextSnapshot:Snapshot=CurrentSnapshot.getNext() in self.A_att=true implies NS.b.B_att=true
ao1:Aop APre:A=a1 APost:A=a2 k:Boolean=true bo1:Bop BPre:B=b2 BPost:B=b3 ret:int=1
a:A b:B Aop() Bop()
s1:Snapshot s2:Snapshot s3:Snapshot A_at :Boao1le:aAn=false B_at :Bobo1le:aBn=false
a2:A A_at :Boolean=true
b2:B B_at :Boolean=false
A_at :Boao3le:aAn=true B_at :Boobl3ea:nB=false In the application model, the designer forgot to specify a postcondition of the Bop to assert that the B_att becomes true, which results in B_att does not become true of the next state in which
A_att becomes true. This violates the specified temporal property.
behavior, which is called a Snapshot Transition Model (ST M ). The ST M is a
class model that characterizes the unfolding of the behavior of the design class
model as valid sequences of state transitions caused by executions of operations.
A state is called a snapshot and it is a structured class that represents a con
guration of objects. The ST M is formed by (1) creating a Snapshot class whose
instances represent states in a transition system, (2) creating a hierarchy of
transition classes that represents operation invocations, (3) converting the
operations' contract conditions to invariants of the transition subclasses, and (4)
de ning traversal query operations between snapshots. The ST M is
mechanically generated from the design class model [
The approach utilizes the snapshots traversal operations to specify and analyze temporal properties in OCL. Speci cally, the operation getNext() returns the next snapshot and the operation getPost() returns the set of all snapshots that come after a snapshot. The operations getPrevious() and getPre() are de ned similarly.
Step2: Interpreting TOCL as OCL property. The unfolding of the transition system of the design class model results in linear traces (sequence of snapshots represented by the ST M ) that can be constrained by OCL. The approach thus interprets the TOCL property, speci ed in the class model, as OCL rstorder constraint that is de ned in the context of the SM T . Fig. 1 shows an example. The TOCL and OCL properties are instances of formal property speci cation patterns, discussed in Section 3.2.
Step 3: Analysis. The approach uses the USE Model Validator [
Step 4: Extracting sequence diagrams. A big number of objects and
transitions produces a counterexample that is complicated and di cult to examine. To
make the analysis result more readable, an algorithm was developed to extract
a sequence diagram from a scenario [
The temporal property speci cation technique
Many software designers nd specifying temporal properties, in a formal
notation, challenging [
This research is validated by applying it to the speci cation and veri cation of
two demonstration case studies [
Future work will concentrate on improving the framework and addressing its limitations. First, the approach is lightweight and only checks nite scenarios; therefore, unbounded liveness properties that require in nite scenarios can not be checked. Investigation will be performed on how the approach can be extended to support such properties. Second, the scalability and the e ciency of the property speci cation and analysis approaches will be investigated. Speci cally, a slicing technique will be developed to verify properties on large class models.