M a is feasible in the on-

Faulty of Information and Natural Sienes

Department of Information and Computer Siene

Vesa Ojala

Counterexample Analysis for Automated

Renement of Data Abstrated State Mahine

Models

Master's thesis submitted in partial fullment of the requirements for the degree of

Master of Siene inTehnology

Espoo,1st Deember2008

Supervisor: Prof. IlkkaNiemelä

Instrutor: Heikki Tauriainen, D.S.(Teh.)

Faultyof Informationand NaturalSienes

Degree Programme of Computer Sieneand Engineering

MASTER'S THESIS

Author

VesaOjala

Date

1stDeember2008

Pages

viii +68

Title ofthesis

Counterexample Analysis for Automated Renement of Data Ab-

strated StateMahineModels

Professorship

Theoretial Computer Siene

Code

T-119

Supervisor

Prof. Ilkka Niemelä

Instrutor

HeikkiTauriainen, D.S.(Teh.)

Statespaeexplosionhasbeenoneofthemainproblemsinmodelhekingwhendealing

with anything but the smallest systems. Dierent abstration tehniques have been

developed to takle this problem. We use data abstration for model heking state

mahinemodelsof objetsommuniating usingasynhronousmessage passingagainst

assertion failures and impliitmessage onsumption.

Whena modelhekerreports aounterexample fromtheabstrat model,theoun-

terexampledoesnotneessarilyorrespondto anexeutionintheoriginalmodel. Suh

spurious ounterexamples need to be identied and theabstration needsto berened

sothat thespurious ounterexample isnolonger possible intheabstratmodel.

In this thesis we desribe a tehnique for identifying spurious ounterexamples. We

also introdue a method for applying dataow analysisto alulate whih of thevari-

ables and objets arerelevant to the ourreneof thespurious ounterexample at dif-

ferentpointsoftheexeution. Theserelevant loations helpustofousonthevariables

needed tobe renedinorderto remove thespuriousounterexample.

We have also developed a method for the automati renement of integer interval

abstrations,aertaintypeofdataabstration. Thismethodusesthenotionofrelevant

loations inthesearh for asuitable renement.

Themethods introdued inthisthesishavebeen implemented intheSMUML(Sym-

boli Methods for UMLBehavioural Diagrams) toolkit.

Informaatio- ja luonnontieteiden tiedekunta

Tietotekniikan tutkinto-ohjelma

TIIVISTELMÄ

Tekijä

VesaOjala

Päiväys

1.joulukuuta2008

Sivumäärä

viii +68

Työnnimi

Vastaesimerkkianalyysi abstrahoituja tietotyyppejä käyttävien tilako-

nemallienautomaattiseen hienonnukseen

Professuuri

Tietojenkäsittelyteoria

Koodi

T-119

Työnvalvoja

Prof. IlkkaNiemelä

Työnohjaaja

Tekn.tri. HeikkiTauriainen

Tarkastettavan järjestelmän tila-avaruuden valtava koko on ollut yksi suurimmista

ongelmista mallintarkastuksessa, pienimpiä järjestelmiä lukuun ottamatta. Ongelman

ratkaisemiseksion kehitetty erilaisia abstraktiotekniikoita. Tässä työssä käytetään ab-

strahoituja tietotyyppejä tarkastettaessa assert-lauseiden pitävyyttä ja implisiittisten

viestinkulutusten olemassaoloa asynkronisestiviestivistätilakonemalleista.

Abstrahoituamalliatarkastettaessasaadutvastaesimerkiteivätvälttämättävastaaai-

nuttakaansuoritustaalkuperäisessämallissa.Tällaisetvalheellisetvastaesimerkittäytyy

tunnistaa ja abstraktiota onhienonnettava valheellisen vastaesimerkin mahdollisuuden

poistamiseksiabstrahoidusta mallista.

Tässä diplomityössä kuvataan, miten valheelliset vastaesimerkit voidaan tunnistaa.

Työssä esitelläänmyös menetelmäoleellisten muuttujien ja olioiden löytämiseensuori-

tuksen kussakin pisteessä tietovuoanalyysiä käyttäen. Nämä oleelliset paikat auttavat

keskittymään muuttujiin, joiden tietotyyppejä hienontamalla saadaan valheellisen vas-

taesimerkin mahdollisuusabstraktiosta poistettua.

Työssä esitelläänmyös menetelmäkokonaislukuvälejäabstrakteina tietotyyppeinään

käyttävienmallien automaattiseenhienonnukseen.Menetelmäetsiisopivaahienonnusta

käyttämällähyväkseenoleellisiapaikkoja.

Työssäesitellytmenetelmätontoteutettu osanaSMUML-projektia(SymboliMeth-

ods for UMLBehavioural Diagrams)osaksi SMUMLtoolkit -ohjelmistoa.

Avainsanat

mallintarkistus,abstrahoiduttietotyypit,abstraktionhienonnus,UML,

tilakoneet

I want to express my gratitude to my instrutor Dr. Heikki Tauriainen for all the

disussions andtheguidaneintheourseofthisstudy. Iwouldalsoliketothankmy

supervisorProf.IlkkaNiemelä. IwanttothankDr.TommiJunttilaforthedisussions

andthesupportduringthisstudy. Finally,Iwouldliketothankmyfamilyandfriends

for the invaluablesupportduring my studies.

Thisworkhasbeenfundedby Tekes(FinnishFundingAgenyforTehnology and

Innovation), Nokia Oyj, Conformiq Software Oy, and Mipro Oy. Their support is

gratefully aknowledged.

Espoo, 1st Deember 2008

Vesa Ojala

1 Introdution 1

2 State Mahine Model 4

2.1 Formal Denitionof a Model. . . 5

2.1.1 Types, Variables,and Expressions . . . 5

2.1.2 Signals, Messages,Queues, and State Mahines . . . 7

2.1.3 Classes, Objets, GlobalCongurations, and Models . . . 8

2.2 Exeution of TransitionComponents . . . 10

2.2.1 Reeiving a Message . . . 11

2.2.2 Sending aMessage . . . 11

2.2.3 Assignment . . . 11

2.2.4 Assertion . . . 12

2.2.5 Movingfroma State to Another. . . 12

2.3 EnabledEvents . . . 12

2.4 Exeution of Events. . . 13

2.4.1 Exeution of TransitionEvents . . . 13

2.4.2 Exeution of Impliit Message Consumption . . . 14

2.4.3 Deferring a Message . . . 14

2.5 Exeutions ina Model . . . 14

3 Model Cheking with Abstrations 16 3.1 Data Abstrations. . . 18

3.1.1 Evaluation of Abstrat Expressions . . . 18

3.2 Formal Denitionof an Abstrat Model. . . 19

3.2.1 Abstrat Types and Variables . . . 19

3.2.2 Abstrat Expressions . . . 20

3.2.3 Abstrat Classes . . . 20

3.2.4 Abstrat Models . . . 21

3.3 Counterexamples . . . 21

4 Feasibility Analysis 25 4.1 Assertion Failures . . . 25

4.2 Impliit Message Consumptions . . . 26

4.3 Ation NotEnabled. . . 26

4.4 Algorithmfor Cheking Feasibility . . . 27

5.1 Forming anAnalysisTrae . . . 29

5.1.1 Transition ExeutionEvents . . . 31

5.1.2 Impliit Consumptions and Message Deferrals . . . 33

5.1.3 Exeution of Ations for Analysis Trae. . . 34

5.2 RelevantLoations . . . 36

5.2.1 InitialRelevant Loations . . . 37

5.2.2 Propagation of RelevantLoations . . . 45

5.3 Rening IntervalAbstrations . . . 51

5.3.1 FindingExpressions for Analysis . . . 52

5.3.2 Analysis of Expressions for Renement . . . 53

6 Implementation 59 6.1 SMUML Toolkit. . . 59

6.2 Counterexample Analyzer inSMUML Toolkit . . . 60

6.3 Conversion from UML 1.4 . . . 60

7 Conlusion 62 7.1 Future Work . . . 62

2.1 Examples of dierent ompoundexpressions. . . 6

2.2 An exampleof a state mahine. . . 8

3.1 Conventional modelheking proedure. . . 16

3.2 Model hekingproedure with abstrationsand abstrationrenement. 17

3.3 The onrete state mahine . . . 22

3.4 An abstrat state mahine . . . 23

4.1 Algorithmis_ounterexample_feasiblehekswhethertheoun-

terexample trae

Trace

^{fromabstrat model}

M a

^{is feasible in the on-}

rete model

M c

^{. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27}

5.1 The algorithm transform forms an analysis trae

L

^{from a spuri-}

ous ounterexample

Trace

^{by simulatingthe exeution inthe onrete}

model

M c

^{and in the abstrat model}

M a

^{. . . . . . . . . . . . . . . . . . 31}

5.2 Algorithm for produing analysis trae steps from the transition exe-

ution events inthe ounterexample trae. . . 32

5.3 Algorithm for produing analysis trae steps from the impliit on-

sumption and message defer eventsin the ounterexample trae. . . 34

5.4 Algorithmfor reatinganalysis traesteps. . . 35

5.5 Funtionomparingthevalueof theonreteexpression oeredtothe

abstrat type tothe value of the orresponding abstrat value. . . 38

5.6 Algorithmfor nding initialrelevant loationsfrom expressions. . . 40

5.7 Algorithmfor nding allthe loationsappearing inthe expression. . . . 41

5.8 Algorithmforreturning atuplerepresenting aloationthe name kind

expression represents. Ifthe onrete andthe abstrat expression does

not represent orrespondingloationsa tuplerepresenting the loation

before the rst non-orresponding loation isreturned. . . 42

5.9 Algorithmfor hekingorrespondene of targetobjets insignal send

ations. . . 43

5.10 Algorithmforalulatinginitialrelevantloations. Thealgorithmtakes

ananalysis trae

T e

^{as argument andreturnsa set ofrelevantloations}

R

^{ontaining the initialrelevant loations. . . . . . . . . . . . . . . . . 44}

5.11 Algorithmfor propagating relevant loations.. . . 46

5.12 Algorithm fornding loations used inthe evaluationof a pair of or-

respondingexpressions. . . 50

5.13 Algorithmforndingexpressions wherethe renements are searhed for. 52

5.15 Algorithmfor ndingallthe loationsin the expression with atypeint. 57

5.16 Algorithmfor evaluatingallint typesubexpressions ofthe expression

given. A set of int subexpression values isreturned. . . 58

3.1 Values of variablesin the objet

o a

^{at dierent points of exeution. . . 23}

3.2 Values of variablesin the objet

o c

^{atdierent pointsof exeution. . . . 24}

5.1 Values of variablesin the objet

o a

^{in global}ongurations

C _a ⁱ

^{. . . . . . 36}

5.2 Values of variablesin the objet

o c

^inglobal ongurations

C _c ⁱ

^{. . . . . . 36}

Introdution

With eah passing year software systems are beoming more and more ompliated.

The more ompliated they beome, the harder it is to ahieve bug-free systems.

Formal veriation methods [11℄ like model heking [12℄ have been developed for

ahieving better quality produts. Although model heking tehniques have been

applied diretlytothe soureode ofsoftware system [14, 37, 8,27℄, it isommonto

onstrutamodelrepresentingthelogiofthesystemwhilehidingsomeofthedetails

inthe realsystem and thenapply modelhekingprograms [9,29℄tothe onstruted

model.

OnewidelyusedmodellinglanguageusedformodellingofsoftwaresystemsisUni-

ed ModellingLanguage (UML) [2,1℄. The researhresulting inthis thesis has been

done inthe SymboliMethodsforUML BehaviouralDiagrams(SMUML)projetde-

velopingmodelhekingtehniquesforUMLmodelsintheLaboratoryforTheoretial

Computer Siene at Helsinki University of Tehnology. Thus all the tehniques de-

sribed inthis thesis have been developed to be part of a model heking framework

for UML models. In this thesis we fous on UML features for speifying the behav-

ior of systems: systems are supposed to be desribed with objets of lasses whose

behavior have been desribed with state mahines. The UML does not x an ation

language for state mahines. A Java-likeation language Jumbala [18℄ is used as an

ation language of state mahines.

Thehugesizeofthestatespaeallbutthesmallestsystemstendtohaveisamajor

problemformodelhekers[36℄. Dierentabstrationtehniqueshavebeendeveloped

to takle this state spae explosionproblem. The idea inabstration tehniques isto

simplifythe modelinordertoreduethe statespae ofthemodel. Thesimpliation

is onstruted in suh a way that some of the harateristis of the original model

are preserved andthusitis possibletoprove somepropertiesfromthe originalmodel

by using the abstrated model. In the SMUML projet we onsidered the use of

twoommonly usedabstration tehniques. Thesetehniques are prediate and data

abstration. In SMUML projet data abstrations were hosen (for the reasons, see

Chapter 3).

Intuitivelyindataabstrationsthedomainsofvariablesarereplaedwithabstrat

in atualomputations. Twologial ways of dening abstrat operators are todene

theoperatorsasover-approximationsorunder-approximations. Over-approximatively

dened operatorsprodueallthe possibleoutomesofanoperation,forexamplewith

an additionof a negativeand apositiveinteger the outome mightbenegative, zero

or positive. Over-approximativeabstrations do not lose behavior in the abstration

thoughtheymightaddit. Ontheotherhandunder-approximativeabstrationsdonot

add anyextrabehavior,but theymightlosebehaviorintheabstration. Forexample

the addition between a negative and a positive integer an not result negative, zero,

nor positive value beause none of the results is guaranteed to orrespond to the

result of an unabstrated operation. Data abstration an be implemented using

value latties [15℄ or with non-deterministi operators [26, 24℄, the latter being our

hoie.

Our data abstrations are over-approximative abstrations meaning that no be-

havior inthe originalmodelis lostinthe abstrationbut instead the abstrat model

may ontain extra behaviorwith no orrespondingbehavior in the originalmodel. If

a data abstrated model annot violate any assertions or perform impliit message

onsumptions, the originalmodelannot doso either [13℄.

The drawbak of the over-approximative data abstration is that a ounterexam-

ple demonstrating a property violation in the abstrat model does not allow us to

automatially onlude that there is an exeution violating the property in the orig-

inal model. The ounterexample might demonstrate a property violating exeution

utilizing the extra behavior introdued by the abstration. Counterexamples demon-

strating exeution not possible in the original modelare alled spuriousor infeasible

and ounterexamples demonstrating a real property violation in the original model

are alled true orfeasible. Feasibility analysis [33℄ is used for reognizing true oun-

terexamples fromthe spurious ones.

Whenthe modelhekergivesusaspuriousounterexampleitannotbededued

whether the properties hold in the original model or not. The extra behavior intro-

dued by the abstrationmakesthe spuriousounterexample possible. The existene

of the spurious ounterexample inthe abstrat model prevents us fromgetting more

onlusive results. To get more onlusive results a new abstration with no possi-

bility for the spuriousounterexample an be reated. Beause the ourrene of the

spurious ounterexample wasmade possibleby the extra behaviorintrodued by the

abstration, a logialstep is tomake a new abstration suh that it doesnot inlude

theextrabehaviorwhihmadethespuriousounterexample possibleintherstplae.

The oldabstration an be used as a startingpoint for the new abstration. Ab-

strationrenement[10℄ isa proess ofmodifyingthe oldabstration sothat itmore

aurately aptures the behavior of the originalmodel. The renement an be made

byhandor,withasuitablealgorithm,automatially. Toahievegoodresultswiththe

manual approah the person rening the abstration has to have an understanding

of the abstration tehnique used, the old abstration, the spurious ounterexample

and the original model. In other words rening the abstration manually requires

muh detailed knowledge. With automati abstration renement a fully automati

model heking proedure utilizingabstrations an be onstruted. It an be leftto

alulate its results unsupervised and if it enounters a spurious ounterexample it

true ounterexample demonstratinga realproperty violationinthe originalmodelor

we have veried that the properties hold in the original model. Though in the real

world, after the renement the abstrat model an have too large a state spae and

the model hekingfailsdue tothe lakof suientresoures, oreven therenement

proedure an fail.

Until nowthere has not been an automati renement for data abstrations. Ex-

isting work on data abstrations onlymentions that renement is needed inorder to

ontinue the model heking proedure when spurious ounterexamples are enoun-

tered but desribe no method for the atual renement (see, for example, [33℄). Our

goalwastodevelopalgorithmsfortheanalysisofspuriousounterexamplesandnally

try to develop an automati renement algorithm based on the analysis algorithms.

We introdue the notion of a relevant loation for desribing important variables in

dierent objets whih ontributeto the ourrene of the spurious ounterexample.

The proess of determiningrelevant loationsstarts with an analysis to the point of

exeution where the onrete model does not have any enabled event orresponding

to the abstrat ounterexample. This analysis nds initial relevant loations whih

serve asa startingpointfor our analysis. Next,from the initialrelevantloationswe

propagate relevant loations to other points of the ounterexample trae using data

owanalysis [30℄shaped tothis purpose. Thedata owanalysis anbethoughtofas

applying program sliing [39, 35, 40℄ to the ounterexample. The relevant loations

guide therenementtobe donetothe variableswhoseabstrat domains'impreision

(introdued by abstration) introdued the extra behavior ausing the existene of

the spuriousounterexample.

We have alsodeveloped analgorithm for ndingrenements for intervalabstra-

tions, a subset of data abstrations. An interval abstration splits the set of integers

to aset of intervals suh that everyintegerbelongsto one of the intervalsand noin-

teger belongs to two distint intervals. A suitable renement ompromising between

the likelihood that the abstration is rened enough to remove the spurious oun-

terexample andnottoomuhtoausestatespaeexplosionisfoundby analyzingthe

expressions aeting the values of the relevant loations. The renement splits the

domainsin the intervalabstrated variables tosmallerintervals fromsuitableplaes.

This thesis begins with a denition of a notion for a simple state mahine model

whih will be used throughout the thesis as a target for all the algorithms. This

notion aptures all the importantfeatures of UML models with respet to our algo-

rithms. ThestatemahinemodelisintroduedinChapter2. Chapter 3desribesthe

model hekingproedure with abstrations and the abstrations used in this thesis.

Feasibility analysis is desribed in Chapter 4. Methodsfor alulating relevant loa-

tions and renement for intervalabstrations are desribed in Chapter 5. Chapter 6

desribes the atual implementation and the relationship between the state mahine

models used in this thesis and the UML 1.4 models. Finally, in Chapter 7 we sum-

marize the earlier hapters and disuss possible improvements and urrent problems

State Mahine Model

Systemsexaminedinthisthesisaredesribedwithmodels. Ourdenitionforamodel

has a lotof similaritieswith UML 1.4[1℄models beause the tehniques desribed in

this thesis have been designed and implemented for a subset of UML 1.4. However

we did not want todesribe our algorithmsusing UML models beause UML models

ontain a lot of unimportant detail in regard to tehniques desribed in this thesis.

Conversion from the subset of UML 1.4 models used in the SMUML projet to the

model formalismused in this thesis is straightforward (desribed in Setion6.3).

Amodelontainsasetofativeobjets(instantiatedfromlasses)ommuniating

asynhronously with eah other by sending messages or via shared variables. Every

messagehasatypeandalistofmessageparameters. Objetsanalsoreeiveexternal

messages from the environment. Every lass ontains a set of variables and a state

mahine that desribes the behavior of the objets instantiated from it. Besides the

variablesdesribed bythelass,objetshaveaninputqueueforstoringmessagessent

to the objet and a defer queue fordeferred messages.

A global onguration denes values of the variables, ontent of the queues, and

ative states ina model. Events modify the globalonguration of asystem.

A state mahine onsistsof states and transitions between the states. One of the

states is an initialstate. Transitions have three omponents: a trigger, a guard and

a listof eet statements. Eah one of the omponentsmay be omitted. The trigger

reeivesmessageofasignalspeiedinthe triggerfromthe inputqueue oftheobjet

the state mahine belongs to. The guard is a boolean expression. A transition is

enabled if the objet an reeive a message of a signal speied in the trigger of the

transition and the guard evaluates to true afterthe message has been reeived. The

transitionan beexeuted ifit isenabled. Thenthe messageisreeived and removed

from the input queue of the objet and messageparameters are assigned tovariables

dened by the trigger. Statements in the eet of the transition are exeuted after

the messagehas been reeived.

Therearethreedierentkindsof statements: assignments,statementsforsending

messages and assertions. Assignments assign a value of an expression to a variable,

statements for sending messages send a message to one of the objets in the model,

and assertions ause a runtime error if the boolean expression assoiated with an

assertion evaluatesto false.

If an objet has no transition enabled in the global onguration, it an either

message by moving it to the defer queue of the objet. For messages of eah signal

either impliitonsumption of deferring isallowed depending onthe ativestate.

2.1 Formal Denition of a Model

In the following denition of a model (and also later in the thesis) the following

funtions willbe used for sequenes and sequene manipulation. A nite sequene of

elements

x 1 , . . . , x n

^iswrittenas

hx 1 , . . . , x n i

^{. Innitesequenesare notneededinthis}

thesis, from now on we refer to nite sequene simply by sequene. The empty se-

quene is

hi

^{, every othersequene is non-empty. Funtion}

head (hx 1 , x 2 , . . . , x n i) = x 1

gives the rst element in the non-empty sequene. Funtion

tail(hx 1 , x 2 , . . . , x n i) = hx 2 , . . . , x n i

^{givesthesequenewithitsrstelementremovedfornon-emptysequenes.}

Funtion

last (hx 1 , x 2 , . . . , x n i) = x n

^{givesthe lastelementinthenon-emptysequene.}

Funtion

append (hx 1 , . . . , x n i, y) = hx 1 , . . . , x n , y i

^{givesthe original sequene with an}

elementaddedtotheendofthesequene. Funtion

concat(hx 1 , . . . , x n i, hy 1 , . . . , y m i) = hx 1 , . . . , x n , y 1 , . . . , y m i

^{onatenates two sequenes.}

2.1.1 Types, Variables, and Expressions

A type

d

^{is a set}

{v 1 , . . . , v n }

^{of possible values. For example a boolean type is}

boolean

= {true , false }

^{,and32-bitintegertypeisint}

= {−2 ³¹ , −2 ³¹ +1, . . . , 2 ³¹ −1}

^.

A type is oerible to another type if every value in the type an be represented

unambiguouslyas a value of the other type. Forexample integers in the programing

language C an be thought to be oerible to boolean values in a way that 0 is

oered to false and other values to true. If a type

d 1

^{is oerible to a type}

d 2

^,

coercible(d 1 , d 2 )

^{, then funtion}

coerce (v 1 , d 1 , d 2 ) = v 2

^{gives the} unambiguous value

v 2

orresponding to the type

d 1

^value

v 1

^{inthe type}

d 2

^{. A type}

d

^{is alwaysoeribleto}

itself:

coerce(v, d , d ) = v

^{for all}

v ∈ d

^.

Avariable

var

^{overaset oftypes}

D

^isapair

hname , d i

^,where

name (var ) = name

is the name of the variable,and

type ( var ) = d ∈ D

^{is the type ofthe variable.}

Expressions are represented as Jumbala expression parse trees. Jumbala [18℄ is

a Java-like ation language for UML state mahines. Expressions are divided into

two distint sets of expressions, ompound and terminal expressions. A ompound

expression

e

^{over a set of variables}

Vars

^{is a tuple}

hkind , id , d 1 , d 2 , op, he 1 , . . . , e n ii

^,

where

• kind = kind (e) ∈ {

^ond

,

^infix

,

^unary

,

^tond

}

^{is the kind of the expression}

e

^,

• id

^{is the unique expression identier} distinguishingdierent expressions in the model (aspeialidentierisneededbeausedierentexpressionsanhaveiden-

-

e 1

e 1 e 2

&&

h cond , id , d 1 , d 2 , && , he 1 , e 2 ii ( e 1 ? e 2 : e 3 )

( e 1 && e 2 ) e 3

e 1 e 2

? :

h tcond , id , d 1 , d 2 , ? : , he 1 , e 2 , e 3 ii

Tuple String

Tree Tuple

Tree

h infix , id , d 1 , d 2 , + , he 1 , e 2 ii h unary , id , d 1 , d 2 , - , he 1 ii

e 1 e 2

+ ( e 1 + e 2 ) String (- e 1 )

Figure2.1: Examples of dierent ompound expressions.

• d 2 = opType(e)

^{is the typeonwhihthe operator}

op

^{operates inthe expression}

e

^,

• op = operator (e)

^{is the operator of the expression}

e

^,and

• subexpr (e) = he 1 , . . . , e n i

^isthelistof

e

^'ssubexpressions. Intreerepresentation,

seen inFigure2.1, the rstsubexpression

e 1

^{isthe leftmost subtree, the seond}

subexpression

e 2

^{istheseondleftmostsubtree,andsoon. Forond,infix,and}

unarykindexpressionseverysubexpressionhastobeatypethatanbeoered

to the type onwhihthe operatoroperates,

∀1 ≤ i ≤ n : coercible(type(e i ), d 2 )

^.

For tond kind expressions subexpressions

e 2

^and

e 3

^{have to be of a type}

that an be oered to the type on whih the operator operates,

∀i ∈ {2, 3} : coercible(type (e i ), d 2 )

^,andsubexpression

e 1

^{hastobeabooleantype}expression,

type (e 1 ) =

^boolean.

Compound expressions of a kind unary have one subexpression, ond and infix

have two subexpressions, and tond has three subexpressions. Figure 2.1 ontains

examples ofdierentompound expressions. Thestring representation ofexpressions

is used in some examplesfor the sakeof simpliity.

Aterminalexpression

e

^{overaset ofvariables}

Vars

^isatuple

hkind , id , d , symboli

^,

where

• kind = kind (e) ∈ {

^lit

,

^name

}

^{is the kindof the expression}

e

^,

• id

^{is the unique expression identier} distinguishingdierent expressions in the model (aspeialidentierisneededbeausedierentexpressionsanhaveiden-

tial other omponents),

• d = type (e)

^{is the type ofthe expression}

e

^{, and}

•

^If

kind =

^litthen

symbol ∈ d

^{. Otherwise}

kind =

^name

and symbol

^isasequene

hvar 1 , . . . , var _n i

^{where every}

var _i

^{is a variable from a set of variables}

Vars

^,

type (var n ) = d

^,and

∀1 ≤ i ≤ n − 1 : type (var i ) =

^{referene. Typereferene}

is used for aessing objetsin amodel and isdened later.

Example 2.1. Let expression

e 1

represented as a string be (2 != (5 +

hvar i

^)).

Let

e 1

^'s subexpressions be 2

= e 2

^{and (5 +}

hvari

⁾

= e 3

^{. Let}

e 3

^{'s subexpres-}

sions be 5

= e 4

^and

hvar i = e 5

^{. Then expression}

e 1

^{is formally} represented as

h

^infix

, id 1 ,

^boolean

,

^int

,

^!=

, he 2 , e 3 ii

^{, its} subexpressions are

e 2 = h

^lit

, id 2 ,

^int

,

²

i

^,

and

e 3 = h

^infix

, id 3 ,

^int

,

^int

,

⁺

, he 4 , e 5 ii

^{, and the expression}

e 3

^'s subexpressions are

e 4 = h

^lit

, id 4 ,

^int

,

⁵

i

^,and

e 5 = h

^name

, id 5 ,

^int

, hvarii

^.

2.1.2 Signals, Messages, Queues, and State Mahines

A signal

sig

^{over aset of types}

D

^{isa pair}

hname , paramtypesi

^,where

• name

^{isthe nameof the signal,and}

• paramtypes = params (sig ) = hd 1 , . . . , d _n i

^{is the sequene of parameter types,}

where

∀1 ≤ i ≤ n : d _i ∈ D

^.

A message

msg

^{of a signal}

sig

^{is a tuple}

hid msg , sig, v 1 , . . . , v n i

^{, where}

id _msg

^is

an identier used for separating otherwise idential messages from eah other and

∀1 ≤ i ≤ n : v i ∈ d _i

^when

params (sig) = hd 1 , . . . , d _n i

^.

Amessage queue overaset of signals

Sigs

^{isa(possibly empty) nitesequene of}

messages overthe signals in

Sigs

^{. Let}

queues(D , Sigs)

^{represent allpossible message}

queues over the types

D

^{and the signals}

Sigs

^.

Astate mahine overaset ofvariables

Vars

^{, systemsignals}

SysSigs

^{,and external}

signals

ExtSigs

⁽

Sigs = SysSigs ∪ ExtSigs

^{), isa tuple}

hs _i , S, T, defers , flushi

^{, where}

• s i ∈ S

^{is the initial state,}

• S = states(sm)

^{isthe set of states}

• T

^{isthe set of} transitions

t = htid , s 1 , s 2 , trig , g, eff i

^{between states, where}

tid

^{is the unique transition identier} distinguishing transitions where all the other omponents are identialin the state mahine,

s 1 ∈ S

^{isthe soure state,}

s 2 ∈ S

^isthe destinationstate,

the trigger

trig

^{is either}

ǫ

^{ora tuple of the form}

hsig, hp 1 , . . . , p n ii

^{, where}

sig ∈ SysSigs ∪ ExtSigs

^,

params(sig) = hd 1 , . . . , d _n i

^{, and}

∀1 ≤ i ≤ n : p i ∈ Vars , coercible ( d _i , type (p i ))

^,

g type (g) =

s 1

s 2

ht1, hsig, hvarii, ǫ, hh assign , hvari, ( hvar i + 1) iii

Figure2.2: An example of a state mahine.

∗ h

^send

, sig, he 1 , . . . , e n i, tgt i

^,where

sig ∈ Sigs

^{,messageparametertypes}

are

params (sig) = hd 1 , . . . , d _n i

^{, every}

e i

^{is an expression over the}

set of variables

Vars

^{suh that}

∀1 ≤ i ≤ n : coercible ( type (e i ), d _i ),

and

tgt

^{is an objet referene type} expression,

type ( tgt ) =

^referene

(referene dened later),

∗ h

^assign

, lhs , rhsi

^,where

lhs

^isanameexpression,

rhs

^isanexpression, andthetypeofexpression

rhs

^{anbeoeredtothe typeofexpression}

lhs

^,

coercible ( type ( rhs ), type ( lhs ))

^{, and}

∗ h

^assert

, ei

^,where

e

^{is aboolean typeexpression over the set of vari-}

ables

Vars

^.

• defers

^{is a funtion giving the set of deferrable signals}

defers(s) ⊆ SysSigs

^for

eah state

s ∈ S

^,and

• flush ⊆ S

^{is asubset of the states inthe state mahine. Moving tothese states}

in the state mahine auses the defer queue tobeushed into the input queue.

Input and defer queues are desribed in Setion 2.1.3. For those familiar with

UML, the set

flush

^{isused inthe} implementation of messagedeferral.

Example2.2. InFigure2.2isagraphialrepresentationofastatemahine. Formally

the statemahineis

hs 1 , S, T, defers , flushi

^{,wherethe setof statesis}

S = {s 1 , s 2 }

^and

the set oftransitions

T = {ht1, s 1 , s 2 , trig, ǫ, hstmt ii}

^{. In the graphial}representation the initialstate

s 1

^{is marked with an arrowwith no soure state. The state mahine}

has only one transition. Its trigger is

trig = hsig , hvarii

^{and the only ation in the}

eet is

stmt = h

^assign

, hvari,

⁽

hvar i

^{+ 1)}

i

^{. The behavior of the funtion}

defers

and the ontent of the set

flush

^{are not shown inthe graphial}representation.

2.1.3 Classes, Objets, Global Congurations, and Models

A lass

c

^{over a set of types}

D

^{, system signals}

SysSigs

^{, and external signals}

ExtSigs

is a pair

hVars, smi

^{, where}

• Vars = Vars (c)

^{,the set of variables in}

c

^{,is a set of variables over}

D

^{, and}

• statemachine(c) = sm

^{, the state mahine of}

c

^{, is a state mahine over the}

variables

Vars

^{,the system signals}

SysSigs

^{, and the external signals}

ExtSigs

^.

An objet

o

^{of a lass}

class (o) = c

^{is a pair}

hc, oid i

^{, where}

c

^{is the lass of the}

objet, and

oid = id (o)

^{is the unique identier of the objet} distinguishing it from other instanes of the same lass in the model. Let

Vars (o) = Vars (c)

^{be the set of}

variablesin the lass of whihthe objet isan instane.

Let

O

^{be a set of objets from a set of lasses}

Classes

^{dened over some set of}

types

D

^{,aset ofsystem signals}

SysSigs

^{and asetof externalsignals}

ExtSigs

^{. Theset}

O

^{induesthe setof loations}

Locations

^{,whihontains pairsofobjetsandvariables}

{ho, vari | o ∈ O, var ∈ Vars (o)}

^{. Theseloationsmap variablestotheir values.}

A global onguration

C

^{of a set of objets}

O

^{from a set of lasses}

Classes

^over

types

D

^{and signals}

Sigs

^{, and a set of loations}

Locations

^{indued by}

O

^{is a tuple}

hsn , state, inputqueue, deferqueue , valuationi

^,where

• sn

^{is the sequene number of}

C

^{to trak the order of global} ongurations in sequenes of global ongurations.

• state(o) = s

^{, where}

state

^{is a funtion mapping objets}

o ∈ O

^{to ative states}

s ∈ states ( statemachine ( class (o)))

^,

• inputqueue (o) ∈ queues (D , Sigs)

^{, where}

inputqueue

^{is a funtion mapping an}

objet

o ∈ O

^{toa messagequeue,}

• deferqueue (o) ∈ queues ( D , Sigs )

^{, where}

deferqueue

^{is a funtion mapping an}

objet

o ∈ O

^{toa messagequeue, and}

• valuation (loc) = v

^{, where}

valuation

^{is a funtion mapping loations}

loc = ho, vari ∈ Locations

^tovalues

v ∈ type ( var )

^.

Let

sn(C) = sn

^{bethesequenenumberoftheglobalonguration}

C

^{. Let}

Act(C, o) = state (o)

^{betheativestatein}

o

^{intheglobalonguration}

C

^{. Let}

InputQueue(C, o) = inputqueue (o)

^{betheinputqueue and}

DeferQueue (C, o) = deferqueue (o)

^bethedefer

queue in a global onguration

C

^{. Let}

VarValue(C, o, var) = valuation(ho, vari)

^be

the value of variable

var

^{inthe globalonguration}

C

^.

For a name expression

e

^{, funtion}

resolve (C, o, e) = ho ^′ , var ^′ i

^{gives the loation}

the expression represents. When

e = h

^name

, id , d , hvar 1 , . . . , var _n ii

^and

n ≥ 1

^,

resolve (C, o, e)

=

 

 

 

 

 



ho, var 1 i

^if

n = 1

^,

o ∈ O

^,

var 1 ∈ Vars (o)

^,

type ( var 1 ) = d

resolve(C, o 1 , e 1 )

^if

n ≥ 2

^,

o ∈ O

^,

var 1 ∈ Vars (o)

^,

type (var 1 ) =

^referene,

o 1 = VarValue(C, o, var 1 )

^,

e 1 = h

^name

, id , d , hvar 2 , . . . , var _n ii

For an expression

e

^{, an objet}

o

^{, and a global onguration}

C

^,

eval (C, F, o, e) = v

^{is the value of expression}

e

^{evaluated in a ontext of the objet}

o

^{in the global}

onguration

C

^when

F

^{is used for solving possible} non-deterministi hoies in the

• C init

^{is an initial global} onguration, or simply the initial onguration, of

the model,

sn(C init ) = 1

^{, input and defer queues for all objets in the initial}

onguration are empty, ative state in all objets is the initial state in the

objet's state mahine,

• D

^{is the set of types whih inludes the boolean type boolean}

= {true, false}

and the objet referenetype referene

= O ∪ {null }

^,

• SysSigs

^{isthe set of system signals overthe set of types}

D

^,

• ExtSigs

^{is the set of external signalsover the set of types}

D

^{. Signalsin the set}

of external signals annot have parameters. External signals must be disjoint

from the set of system signals,

SysSigs ∩ ExtSigs = ∅

^,

• Classes

^{is the set of lasses over the set of types}

D

^{, the set of system signals}

SysSigs

^{,and the set of external signals}

ExtSigs

^,

• O

^{is the set of objetsin the model, and}

• Locations

^{is the set of loationsindued by}

O

^.

Example 2.3. A simple model with one lass and one objet instantiated from

the onlylass inthe modelouldbe

hC _init , D , Classes , O, Locations , SysSigs , ExtSigs i

^,

where

• D = {

^int

,

^boolean

,

^referene

}

^,

• SysSigs = ∅

^,

• ExtSigs = {sig}

^,

•

^{a set of lasses}

Classes = {c}

^{ontains only one lass,}

c = h{var }, smi

^{, where}

sm

^{is the state mahine fromFigure2.2,}

•

^asetofobjets

O = {o}

^{ontainstheonlyobjet,}

o = hc, 1i

^,whihisinstantiated from the onlylass inthe model,

• Locations = {ho, vari}

^{, and}

• C init = h1, s 1 , inputqueue , deferqueue , valuationi

^.

For our only objet

inputqueue (o) = InputQueue(C init , o) = hi

^,

deferqueue(o) = DeferQueue(C init , o) = hi

^{, and for the only variable in the objet we an dene,}

for example,

valuation (ho, var i) = 0

^.

2.2 Exeution of Transition Components

Transitions onsist of dierent onguration altering omponents. In this setion

we desribe how these omponents modify the onguration. In Setion 2.4 these

denitions are used when the eets of a transition exeution are introdued. The

exeution of omponents of transitions is partially dened, ases not dened are not

used in the algorithms.

Reeiving a message by a trigger

trig

^{in aglobal onguration}

C

^{inan objet}

o

^pro-

duesanewglobalonguration

C ^′ = exec _recv (C, o, trig)

^where

C ^′

^{isformedaording}

to the followingrules:

•

^If

trig = ǫ

^{, then}

C = C ^′

^,

•

^if

trig = hsig, hp 1 , . . . , p n ii

^and

head (InputQueue(C, o)) = hid msg , sig, v 1 , . . . , v n i

^,

then

C ^′ = C

^{exept that}

The sequene number isinremented:

sn (C ^′ ) = sn (C) + 1

^,

The messageto be reeived is removed from the input queue:

InputQueue(C ^′ , o) = tail (InputQueue (C, o))

^,and

Message parameters are assigned to the variables speied in the trigger:

∀1 ≤ j ≤ n : VarValue(C ^′ , o, p j ) = v j

^.

2.2.2 Sending a Message

The exeutionof asend ation

stmt = h

^send

, sig , he 1 , . . . , e n i, tgt i

^inanobjet

o

^ina

globalonguration

C

^{produesanew globalonguration}

C ^′ = exec _eff (C, F, o, stmt )

where

C ^′ = C

^{exept that:}

•

^{The sequene numberis} inremented:

sn (C ^′ ) = sn(C) + 1

^,

•

^{The objet whih reeives the message is} determined:

o ^′′ = eval(C, F, o, tgt)

^,

•

^{The message isformed and the parameter values are} determined:

msg = hsn(C), sig, v 1 , . . . , v n i, ∀1 ≤ j ≤ n : v j = eval (C, F, o, e j )

^{, and}

•

^{The messageisaddedtothe endofthe inputqueue oftheobjetwhihreeives}

the message:

InputQueue (C ^′ , o ^′′ ) = append ( InputQueue (C, o ^′′ ), msg )

^.

2.2.3 Assignment

Exeuting an assign ation

stmt = h

^assign

, lhs , rhsi

^{in an objet}

o

^{in a global on-}

guration

C

^{produes a new global onguration}

C ^′ = exec _eff (C, F, o, stmt)

^where

C ^′ = C

^{exept that:}

•

^{The sequene numberis} inremented:

sn (C ^′ ) = sn (C) + 1

^{, and}

•

^Thevalue

v = eval(C, F, o, rhs)

^{isassignedtoaloationindiatedby}

ho ^′′ , vari =

resolve (C, o, lhs)

^:

VarValue(C ^′ , o ^′′ , var) = v

^.

The exeution of an assertion ation

stmt = h

^assert

, ei

^{in an objet}

o

^{in a global}

onguration

C

^{produes a new global onguration}

C ^′ = exec _eff (C, F, o, stmt )

^suh

that:

•

^{If the ondition in the assertion statement evaluates to true,}

eval(C, F, o, e) = true

^{, then}

C ^′ = hsn + 1, state, inputqueue, deferqueue , valuation i

^{, when}

C = hsn , state , inputqueue , deferqueue , valuation i

^,or

•

^else

C ^′ = ⊥

^{, where}

⊥

^{is a speial value indiating an assertion error in the}

exeution.

2.2.5 Moving from a State to Another

Movingto astate

s

^{in aglobal onguration}

C

^inanobjet

o

^{produesa new global}

onguration

C ^′ = exec _goto (C, o, s, b)

^when

b = true

^if

s ∈ flush

^{, otherwise}

b = false

^,

and where

C ^′ = C

^{exept that:}

•

^{The sequene numberis} inremented:

sn (C ^′ ) = sn(C) + 1

^,

•

^{The ative state of objet}

o

^{isset tothe new state:}

Act (C ^′ , o) = s

^,and

•

^{The messages in}

o

^{'s defer queue are moved to the beginningof}

o

^{'s input queue}

if

b = true

^:

InputQueue(C ^′ , o) = concat(DeferQueue(C, o), InputQueue(C, o))

and

DeferQueue(C ^′ , o) = hi

^{, otherwise}

InputQueue(C ^′ , o) = InputQueue (C, o)

and

DeferQueue (C ^′ , o) = DeferQueue (C, o)

^.

2.3 Enabled Events

Exeution in the modelproeeds by exeution of events. Events are atomi, in par-

tiular the exeution of a transition onsists of several steps exeuted together as a

single atomi event. An event an be exeuted onlyif it is enabled.

In aonguration

C

^atransition

t = htid , s 1 , s 2 , trig, g, eff i

^{exeutionevent inan}

objet

o

^,

a = h

^trans

, F, o, ti

^{, isenabled,}

enabled (C, a)

^,if:

•

^{The soure state}

s 1

^{of the transitionisan ativestate:}

Act (C, o) = s 1

^,

•

^{The trigger is empty,}

trig = ǫ

^{, or there is a message of a signal} orresponding to the trigger in the head of

o

^{'s input queue:}

trig = hsig, hp 1 , . . . , p n ii

^when

head ( InputQueue (C, o)) = hid msg , sig , v 1 , . . . , v n i

^{, and}

•

^{The triggeris empty and the guard evaluatesto truein the onguration}

C

^,or

the trigger is non-empty and the guard evaluates to true in the onguration

C ^′ = exec _recv (C, o, trig)

^{whih would result from reeiving the message in the}

onguration

C

^.

In onguration

C

^{deferring a message}

a = h

^defer

, oi

^{inan objet}

o

^{is enabled,}

enabled (C, a)

^{, if:}

•

^{The input queue of}

o

^{isnot empty:}

|InputQueue (C, o)| > 0

^,

•

^{The objet}

o

^{has noenabled}transitions:

∀t ∈ T : ¬enabled(C, h

^trans

, F, o, ti)

^,

when

T

^{isthe set of} transitions inthe state mahine of the objet

o

^,

•

^{The message atthe head of}

o

^{'s input queue an be deferred inthe ative state:}

sig ∈ defers (Act (C, o))

^{, when}

head (InputQueue (C, o)) = hid msg , sig, v 1 , . . . , v n i

^.

In onguration

C

^{, the exeution of an impliit message onsumption event}

a = h

^impl

, oi

^{inan objet}

o

^{is enabled,}

enabled (C, a)

^{, if:}

•

^{The input queue of}

o

^{isnot empty:}

|InputQueue(C, o)| > 0

^,

•

^{The objet}

o

^{has noenabled}transitions:

∀t ∈ T : ¬enabled (C, h

^trans

, F, o, ti)

^,

when

T

^{isthe set of} transitions inthe state mahine of the objet

o

^,

•

^{Themessageattheheadof}

o

^{'sinputqueueannotbedeferredintheativestate:}

sig ∈ / defers (Act (C, o))

^{, when}

head (InputQueue (C, o)) = hid msg , sig, v 1 , . . . , v n i

^.

No event isenabled if

C = ⊥

^.

2.4 Exeution of Events

Exeutions of events alter the global ongurationin the followingways.

2.4.1 Exeution of Transition Events

Theexeutionofanenabledtransitionexeutionevent

a = h

^trans

, F, o, ti

^,where

t = htid , s 1 , s 2 , trig, g, eff i

^{,inaglobalonguration}

C

^{produesanewglobalonguration}

C ^′ = exec(C, a)

^{by the following steps:}

•

^{First the objet reeives a message} orresponding to the trigger's signal:

C t = exec _recv (C, o, trig)

^,

•

^{Then everyation in}

eff = hstmt 1 , . . . , stmt _n i

^{is exeuted:}

C 1 = exec _eff (C t , F, o, stmt 1 )

∀2 ≤ i ≤ n : C i = exec _eff (C i− 1 , F, o, stmt _i )

Ifsome ationproduesaglobal onguration

⊥

representing anassertion error,then theexeutionishaltedand the resultingglobalongurationis

set to

C ^′ = ⊥

^,

•

^{The objet moves from the state}

s 1

^{to the state}

s 2

^:

C ^′ = exec _goto (C n , o, s 2 , b)

^,

where

b = true

^if

s 2 ∈ flush

^{, otherwise}

b = false

^.

The exeution of anenabled impliit messageonsumption event

a = h

^impl

, oi

^{, in a}

globalonguration

C

^{produesanewglobalonguration}

C ^′ = exec (C, a)

^suhthat:

•

^{The sequene numberis} inremented:

sn (C ^′ ) = sn(C) + 1

^,

•

^{The message tobe onsumed is removed fromthe input queue:}

InputQueue (C ^′ , o) = tail (InputQueue(C, o))

^,

•

^{Everything else is like itwas before the message wasonsumed:}

∀o ^′ ∈ O : ∀var ∈ Vars (o ^′ ) : VarValue(C ^′ , o ^′ , var ) = VarValue(C, o ^′ , var)

∀o ^′ ∈ O \ {o} : InputQueue (C ^′ , o ^′ ) = InputQueue(C, o ^′ )

∀o ^′ ∈ O : DeferQueue (C ^′ , o ^′ ) = DeferQueue (C, o ^′ )

∀o ^′ ∈ O : Act (C ^′ , o ^′ ) = Act (C, o ^′ )

^.

2.4.3 Deferring a Message

The exeutionof an enabled messagedefer event

a = h

^defer

, oi

^,

enabled (C, a)

^{,in a}

globalonguration

C

^{produesanewglobalonguration}

C ^′ = exec (C, a)

^suhthat:

•

^{The sequene numberis} inremented:

sn (C ^′ ) = sn(C) + 1

^,

•

^{The message tobe deferred is removed from the input queue:}

InputQueue (C ^′ , o) = tail (InputQueue(C, o))

^,

•

^{The message isadded to the defer queue:}

DeferQueue (C ^′ , o) =

append (DeferQueue(C, o), msg)

^,when

InputQueue (C, o) = hmsg, . . .i

^,

•

^{Everything else is like itwas before the message wasdeferred:}

∀o ^′ ∈ O : ∀var ∈ Vars (o ^′ ) : VarValue(C ^′ , o ^′ , var ) = VarValue(C, o ^′ , var)

∀o ^′ ∈ O \ {o} : InputQueue (C ^′ , o ^′ ) = InputQueue (C, o ^′ )

∀o ^′ ∈ O \ {o} : DeferQueue (C ^′ , o ^′ ) = DeferQueue (C, o ^′ )

∀o ^′ ∈ O : Act (C ^′ , o ^′ ) = Act (C, o ^′ )

2.5 Exeutions in a Model

An exeution in a model

M = hC _init , D , Classes , O, Locations , SysSigs , ExtSigsi

^{is a}

sequene

trace = hb 1 , . . . , b n i

^{, where}

b i = hC i , a i , C i +1 i

^,

1 ≤ i ≤ n

^{, suh that}

• ∀1 ≤ i ≤ n : a i

^{is a transitionexeution event, an impliit onsumptionevent,}

or amessage defer event,

• ∀1 ≤ i ≤ n + 1 : C i

^{is aglobal} onguration,

• C 1 = C init

• ∀1 ≤ i ≤ n : enabled (C i , a i )

^.

• ∀1 ≤ i ≤ n : C i +1 = exec(C i , a i )

Model Cheking with Abstrations

The objetive in modelheking [12℄ is tohek whether some properties, whih are

for some reasoninteresting to the user, hold in the modelto bemodelheked. The

modelheker takesa modeland aset of propertiesas aninputand outputs eithera

message that the properties hold in the model orgives a ounterexample illustrating

anexeutioninthemodelthatviolatesoneoftheproperties. Figure3.1illustratesthe

normalmodelhekingproedure. Inthisthesisthe propertiesweare modelheking

against are the absene of assertionfailures and impliit messageonsumptions.

The need for abstration tehniques arises from the huge size of the state spae

all but the smallest models tend to have. The phenomenon is alled state spae

explosion [36℄. Dierent abstration tehniques have been developed to takle this

problem. In abstration the idea is to reate another model, abstrat model, whih

represents the behavior of the original model but abstrats away some details from

the original model to redue the size of its state spae. Then the abstrat model is

heked with a model heker for the same properties that we are interested in the

original model.

The abstrat modelis onstruted in suh a way that some of the harateristis

of the original modelare preserved thus making it possible toprove some properties

fromtheoriginalmodelbyusingtheabstratmodel. Forexample,over-approximative

abstration tehniques add behavior tothe abstrat modelompared tothe onrete

model but all the behaviors in the onrete model have a orresponding behavior in

the abstrat model. Therefore if theabstrat modelreatedinanover-approximative

manner does not ontain assertion failures, then the orresponding onrete model

does not ontain assertion failures either [13℄. On the other hand if the abstrat

modelontainsassertionfailures, weannottellwithoutfurtheranalysis whether the

onrete modelontainsassertionfailuresbeausetheover-approximativeabstration

Model checker

Properties Counterexample

Model Properties hold

Figure3.1: Conventional model heking proedure.

Abstract model

Spurious counterexample Concrete model

Abstraction Properties

Properties hold

True counterexample Abstract

model generation

Refinement Abstract

counterexample

Counterexample analysis

Model checker

Feasibility analysis

Figure 3.2: Model hekingproedure with abstrationsand abstrationrenement.

might have added new behaviorsto the abstrat model.

The proess for determining whether an abstrat ounterexample orresponds to

an exeution in the onrete model is alled feasibility analysis [33℄. If an abstrat

ounterexample has a orresponding exeution in the onrete modelthen the oun-

terexample is alled feasible, otherwise it is spurious. The exeution of a spurious

ounterexample inthe abstrat modelviolates the properties but itsexeutionin the

onrete model does not or the orresponding exeution is not even possible in the

onrete model. An example of a spurious ounterexample an be found in Setion

3.3.

Even ifaspuriousounterexampleisenountered,wewanttoeitherprovethatthe

properties hold in the onrete modelor that there is atrue ounterexample demon-

stratingthatapropertydoesnotholdintheonretemodel. Tobeabletodothis,we

have torene [10℄ the abstration (makethe abstration more preise). The purpose

of renement istohange theabstration inaway that the spuriousounterexample

doesnotappearintheabstrat modelonstrutedwiththerened abstration. After

the abstration is rened, a new abstrat model is produed with the new abstra-

tion and the whole proess starts again. The renement an be done by hand or

automatially. In our ase the ounterexample analysis desribed in Setion 5 ana-

lyzes automatiallythe way the abstration needs tobe rened. The modelheking

proedure with abstrationsand abstrationrenement isshown inFigure3.2.