Model checking contracts : a case study

Department of Informatis

Model Cheking

Contrats

A Case Study

Researh Report No.

362

Gordon Pae

Cristian Prisaariu

Gerardo Shneider

Isbn 82-7368-320-6

Issn 0806-3036

August 2007

Updated: September 2007

A Case Study

∗

Gordon Pae

†

, Cristian Prisaariu

‡

, Gerardo Shneider

§

August 2007

Updated: September 2007

Abstrat

Contrats areagreements between distint parties that determine

rightsand obligations on their signatories, and have been introdued

inordertoreduerisksandto regulateinter-businessrelationships. In

this paperwe showhowaonventional ontrat anbewritten inthe

ontrat language

CL

^{,howto modelthe ontrat, and nallyhow to}

verifyproperties ofthe modelusing theNuSMVmodelheking tool.

1 Introdution

Internet-based appliations involving one or more entities partiipating in

inter-business ollaborations, virtual organisations, and web servies, usu-

ally ommuniate through servie exhanges. Suh exhanges are subjet

to ertain understanding onthe dierent roles the partiipants play, inlud-

ing assumptions on their orret and inorret behaviours, and their rights

and obligationsin order toavoid misunderstanding and ambiguities insuh

business relationships. Thismotivatesthe needof establishinganagreement

before any transation is performed, through a ontrat, guaranteeing the

∗

Partiallysupportedby theNordunet3 projetContrat-OrientedSoftwareDevelop-

mentforInternetServies. Thisisarevisedand extendedversionofthepaperwiththe

sametitlesubmittedtoATVA'07 andpublishedin LNCSno. 4762.

†

Dept. of Computer Siene and AI, University of Malta, Msida, Malta. E-mail.

gordon.paeum.edu.mt

‡

Dept. ofInformatis, Univ. of Oslo. P.O. Box1080 Blindern, N-0316Oslo, Norway.

E-mail: ristii.uio.no

§

Dept. ofInformatis, Univ. of Oslo. P.O. Box1080 Blindern, N-0316Oslo, Norway.

E-mail: gerardoi.uio.no

determining penalties inase of ontrat violations, and be asunambiguous

as possible to avoid oniting interpretations. Conventional ontrats are

douments written in naturallanguage, as one may nd inusual judiial or

ommerialtraditionalativities. Onthe otherhand,eletroni ontrats(or

e-ontratsforshort)aremahine-orientedandassuhthey mustbeunder-

stood by thesoftware responsiblefor ontrolling andmonitoringthe servie

exhanges. E-ontrats might be seen in two dierent ways: (1) As the ex-

eutable version of a onventional ontrat, obtained from the translation

of the paper version into the eletroni one; (2) As ontrats by them-

selvesobtained diretlyfrom ertain software appliations, likeweb servies

and virtual organisations. Forour urrent purposes, the dierene above is

irrelevant,though our ase study is based ona onventional ontrat.

Ideally, e-ontrats should be shown to be ontradition-free both inter-

nally,and with respet tothe governingpoliiesunder whih the ontratis

enated. Moreover, there must be arun-time system ensuring that the on-

trat is respeted. In other words, ontrats should be amenable to formal

analysis allowingboth stati anddynamiveriation, andthuswrittenina

formal language. In this paper we are interested only in the analysis of the

ontrat itself (statially), and we are not onerned with its relation with

poliiesnor with its enforement atrun-time.

A formal language for writing ontrats should be designed as to avoid

most of the philosophial problems of deonti logi [MN06 ℄. Moreover,

it should be possible to represent onditional obligations, permissions and

prohibitions, as well as ontrary-to-duty obligations (CTD) and ontrary-

to-prohibitions (CTP). CTDs are statements representing obligations that

might not be respeted, whereas CTPs are similar statements dealing with

prohibitions that might be violated. Both onstrutions speify the obli-

gation/prohibition to be fullled and whih is the reparation/penalty to be

applied inase of violation.

A formal language for writing (untimed) ontrats is

CL

^{[PS07℄. The}

language is tailored toe-ontrats, followingan ation-based approah, and

having the following properties: (1) The language avoids most of the lassi-

al paradoxes of deonti logi; (2) It is possible to express in the language

(onditional) obligations, permissions and prohibitions over onurrent a-

tions keepingtheir intuitivemeaning; (3) It ispossible toexpress CTDs and

CTPs; (4) The language has a formal semantis given in a variant of the

modal

µ

^-alulus.

Themain ontributionofthis paperistoshowhowmodelheking teh-

niques an be applied in the ontext of ontrat-oriented software develop-

ment, in order to determine whether a given ontrat stipulates what it is

supposed to.

CL

^{is used as an} intermediate language between the ontrat inplainEnglishand the systemspeiationrequired bythe modelheking

tool. Thisuse of

CL

^{inreases the ondeneintheinitial}formulationof the ontrat lauses. The model heking method that we present requires to

pursue the followingsteps:

1. Model the onventional ontrat written in English into the formal

language

CL

^;

2. Translatesyntatiallythe

CL

^{speiationintotheextended}

µ

^-alulus

C µ

^;

3. Obtain a Kripke-like model (a labelled transition system with state

propositions LTS) of the

Cµ

^formulae;

4. Translate the LTS intothe inputlanguage of NuSMV;

5. Perform modelheking using NuSMV;

6. In ase of a ounter-example given by NuSMV, interpret it as a

CL

lause andrepeat the modelheking proess until theproperty issat-

ised;

7. Finally, repair the original ontrat by addinga orresponding lause,

if appliable.

This tehnial report is an extended and revised version of the paper

[PPS07 ℄. The ontent is essentially the same with the exeption of more

detailed explanationsand the orretions of fewtyposappearing inthe on-

ferene paper. We have added a footnote explaining the error in the orre-

sponding plae.

Thepaperisorganised asfollows. InSetion2westart bypresenting the

language

CL

^{, inluding an example of the kind of ontrats we are dealing}

with, fromwhih we will extrat our ase study. Setion 3 is the main part

ofthepaperwherewerst formalisetheasestudy in

CL

^{,andafterwardswe}

showhow touse modelheking and the NuSMVtooltodetermine whether

the ontrat is orret with respet to ertain desired properties, and how

to get feedbak as to write the orret ontrat. In Setion 4 we analyse

related works and onlude by disussing our hoie of the model heking

tool aswellas future work.

We present in Fig. 1 a part of a onventional ontrat between a servie

provider and a lient, where the provider gives aess to Internet to the

lient. We analyse part of this ontrat in the following setion. First we

reall the ontrat language

CL

^{;for amore detailed}presentationsee [PS07℄.

Denition 2.1 A ontrat is dened by:

Contract := D ; C

C := φ | C O | C P | C F | C ∧ C | [α]C | hαiC | C U C | C | C C O := O(α) | C O ⊕ C O

C P := P (α) | C P ⊕ C P

C F := F (δ) | C F ∨ [δ]C F

Thesyntax of

CL

^{loselyresembles thesyntaxof amodal(deonti) logi.}

Though this similarity is learly intentional sine we are driven by a logi-

based approah,

CL

^{is not a logi. The semantis of}

CL

^{are given in an}

extensionof

µ

^{-alulus[Koz83℄whihweall}

Cµ

^{. Inwhat follows weprovide}

an intuitiveexplanation of the

CL

^syntax.

A ontrat onsists of two parts: denitions (

D

^{) and lauses (}

C

^{). We}

deliberately let the denitions part underspeied in the syntax above.

D

speies the assertions(or onditions) andthe atomiationspresent inthe

lauses.

φ

^{denotes assertions and rangesover boolean} expressions inluding the usual boolean onnetives, and arithmeti omparisons like the budget

is morethan200$.

1

We lettheatomiations underspeied, whihfor our

purposes an be understood as onsisting of three parts: the properation,

thesubjetperformingtheation,andthetargetof(or,the objetreeiving)

suh anation. Notethat, inthis way, the partiesinvolved inaontrat are

enoded in the ations.

C

^{isthe general ontrat lause.}

C O

^,

C P

^,and

C F

^denoterespetively obli-

gation, permission, and prohibition lauses.

O(·)

^,

P (·)

^,and

F (·)

^{, represents}

the obligation, permission or prohibition of performing a given ation.

∧

and

⊕

^{maybethoughtasthelassialonjuntionandexlusive}disjuntion, whihmay beused toombine obligationsand permissions. Forprohibition

C F

^{we have}

∨

^{, again with the lassial meaningof the} orresponding opera- tor.

α

^{is a ompound ation (i.e., an expression ontaining one or more of}

1

Wehavekeptthesyntaxof

CL

^{asitappearsintheoriginalpaper.} Assertions,denoted by

φ

^{, are howeverredundantasthey donot make sense as}stand-alone lauses. Weare urrentlyworking ontheimprovementof thelanguage

CL

^{to addressthis and fewother}

designdeisions.

the following operators: hoie

+

^{; sequene}

·

^{; onurreny}

&

^{, and test}

?

^{see[PS07℄),while}

δ

^{denotes aompoundationnot ontaininganyo-}

urreneof

+

^{. Notethat}syntatially

⊕

^{annotappearbetween}prohibitions and

+

^{annot our under the sope of}

F

^.

We borrow from propositional dynami logi [FL77℄ the syntax

[α]φ

^to

representthatafterperforming

α

^{(ifitispossibletodoso),}

φ

^{musthold. The}

[·]

^{notationallows havingatest, where}

[φ?]C

^{must beunderstoodas}

φ ⇒ C

^.

hαiφ

^{aptures the idea that itexists the} possibility of exeuting

α

^{,in whih}

ase

φ

^{must hold} afterwards. Following temporal logi (TL) notation we have

U

^(until),

^{(next), and}

^{(always), with intuitive semantis as in}

TL[Pnu77℄. Thus

C ₁ U C ₂

^statesthat

C ₁

^{holds until}

C ₂

^holds.

C

intuitively statesthat

C

^{holdsinthenextmoment,usuallyaftersomethinghappens,and}

C

^{expressing that}

C

^{holdsineverymoment. Wean dene}

♦ C

(eventually)

for expressing that

C

^{holds sometimes in afuture moment.}

To express CTDs we provide the following notation,

O ϕ (α)

^{, whih is}

syntati sugar for

O(α) ∧ [α]ϕ

^{stating the obligation to exeute}

α

^{, and}

the reparation

ϕ

^{in ase the obligation is violated, i.e. whenever}

α

^{is not}

performed. The reparation may be any ontrat lause. Similarly, CTP

statements

F ϕ (α)

^{an be dened as}

F ϕ (α) = F (α) ∧ [α]ϕ

^{, where}

ϕ

^{is the}

penalty in ase the prohibition is violated. Notie that it is possible to

express nested CTDs and CTPs.

In

CL

^{we an write onditional}obligations, permissions and prohibitions in two dierent ways. Just as anexample letusonsider onditionalobliga-

tions. The rst kindisrepresented as

[α]O(β)

^{,whihmay be readas after}

performing

α

^{, one is obliged to do}

β

^{. The seond kind is modelled using}

the test operator

?

^:

[ϕ?]O(α)

^, representing If

ϕ

^{holds then one is obliged}

to perform

α

^{. Similarly forpermissionand} prohibition. Foronveniene, in what follows we use the notation

φ ⇒ C

^{instead of the}

CL

^syntax

[φ?]C

^.

3 A Contrat Case Study

In what followswe onsider part 7 of the ontrat given inFig. 1 between a

servie providerand a lient, wherethe providergivesaessto the Internet

to the lient. We onsider two parameters of the servie: high and normal,

whihdenotethelient'sInternettra. Wewillonsideronlythe following

lauses of the ontrat.

7.1. TheClientshallnot:

a) supplyfalseinformationtotheClientRelationsDepartmentoftheProvider.

7.2. WhenevertheInternetTraishighthentheClientmustpay

[price]

immediately,ortheClient mustnotifytheProviderbysendingane-mailspeifyingthathewillpaylater.

theInternettratothenormallevel,andpaylatertwie(

2 ∗ [price]

^).

7.4. If theClientdoesnotlowerthe Internet traimmediately,then the Clientwillhavetopay

3 ∗ [price]

^.

7.5. The Clientshall, as soon as the Internet Servie beomesoperative, submit within seven (7)

daysthePersonalDataFormfromhisaountonthe Provider'swebpagetotheClientRelations

DepartmentoftheProvider.

Wealsoadd lause11.2asitisstrongly relatedtolause7.1andthe two

should be taken together:

11.2. Providermay,atitssoledisretion,withoutnotieorgivinganyreasonorinurringanyliability

fordoingso:

b) SuspendInternetServiesimmediatelyifClientisinbreahofClause7.1;

In what follows we formalise the above ontrat lauses. As part of the

formalisation of a ontrat in

CL

^{we rst have to dene the assertions and}

ations:

φ

^{= the Internet tra ishigh}

f i

^{= lient suppliesfalse} informationtoClientRelations Department

h

^{= lient inreases Internet tra tohigh level}

p

^{= lient pays [prie℄}

d

^{= lient delays payment}

n

^{= lient notiesby e-mail}

l

^{= lient lowers the Internet tra}

sf D

^{= lient sends the Personal DataForm toClientRelations Department}

o

^{= provider ativates the Internet Servie (itbeomesoperative)}

s

^{= provider suspends servie}

Note that we have the ation

h

^{whih does not appear expliitly in the}

example lauses. Ation

h

^{is impliit as it makes the} proposition

φ

^valid

(the Internet beomes high only if the lient inreases it). Ation

h

^{an be}

onsidered as the omplement of ation

l

^{whih makes}

φ

^{false (lowers the}

Internet tra). The six lauses aboveare writtenin

CL

^{as follows:}

1.

F P (s) (f i)

2.

[h](φ ⇒ O(p + (d&n)))

3.

([d&n](O(l) ∧ [l] ♦ O(p&p)))

4.

([d&n · l ] ♦ O(p&p&p))

5.

([o]O(sf D))

Clause 1 has a onise syntax and represents a ontrary-to-prohibition.

More preisely, the CTP represents the prohibition

F (f i)

^{(lause 7.1) and}

the reparation whih should be enfored in ase the prohibition is violated

(in this ase

P (s)

^{; the right of the provider to suspend the Internet servie,}

lause 11.2).

Note that all the lauses are supposed to hold throughout the whole

ontratbeauseofthe

^{. Clause2modelslause7.2oftheontratexample}

and it represents the fat that whenever the assertion

φ

^{holds (the Internet}

traofthelientisatthehighlevel)thenitmustbetheasethatthelient

is obliged to hoose (

+

^{) between either paying} immediately (

p

^{) or delaying}

the payment by sendingthe notiation (

d&n

^).

Clauses3 and 4 referto the lauses 7.3 and 7.4of the ontrat example.

They both refer to the moment after the lient has delayed the payment

(

[d&n]

^{). Clause 3 states that the lient has the obligation to lower the In-}

ternet tra (

O(l)

^{) and that after lowering the lient should pay twie the}

prie. On the other hand, lause 4 speies the obligation of the lient

to pay three times the prie in ase he does not lower the Internet tra

(

l

^{). The two formulae may be ombined in a single formula using CTDs:}

([d&n](O ϕ (l) ∧ [l] ♦ (O(p&p))

^where

ϕ = O (p&p&p)

^{. Clause5formallyrep-}

resents lause 7.5 of the ontrat example. It represents the obligation of

the lient to submit the form (

O(sf D)

^{) after the Internet servie beomes}

operative (

[o]

^).

3.1 Translating the

CL

^{speiation into}

C µ

We extrat a model from the

CL

^{lauses by rst} translating the language speiation into the extended

µ

^-alulus

Cµ

^{where the semantis is given}

as a speial labelled transition system. The translation funtion

f ^T

^whih

takesa

CL

^{formulaandreturnsaformulainthe}

C µ

^{isshown inTable 1. The}

speial syntax

[any]

^{(or the dual}

hanyi

^{) represents the fat that any ation}

an beexeuted. Torepresent obligationsand prohibitions ofa given ation

a

^{we need the speial} propositionalonstants

O a

^and

F a

^.

We brieymention here thesemantis of

C µ

^{, see [PS07 ℄for moredetails.}

The formulae are interpreted over a labelled transition system (LTS). The

labelsofthetransitionsarerepresentedbymulti-setsofations(e.g.

{p, p, p}

is a label orresponding to the

CL

^{onurrent ation term}

p&p&p

^{). The}

formulae are interpreted over states asusual in modallogis with semantis

on LTSs. For example the expression

φ ⇒ hpiO p

^is interpreted in a state and shouldbeunderstoodas: ifthe assertion

φ

^{holdsinthestatethen}

hpiO p

shouldholdinthesamestate.

[p]C

^and

hpiC

^areinterpretedasholdinginthe urrentstateifandonlyifinthenextstatereahablebyation

p

^theformula

orrespondingtothetranslationof

C

^{holds. In}

Cµ

^{thedierenebetween the}

two operators is that

hpiϕ

^{requires the existene of at least one next state}

reahable by

p

^where

ϕ

^{holds, where}

[p]ϕ

^{is quantied} universally, and thus

(1)

f ^T (O (& ⁿ _i=1 a i )) = h{a 1 , . . . , a n }i(∧ ⁿ _i=1 O a i )

(2)

f ^T (C O ⊕ C O ) = f ^T (C O ) ∧ f ^T (C O )

(3)

f ^T (P (& ⁿ _i=1 a i )) = h{a 1 , . . . , a n }i(∧ ⁿ _i=1 ¬F a i )

(4)

f ^T (C P ⊕ C P ) = f ^T (C P ) ∧ f ^T (C P )

(5)

f ^T (F (& ⁿ _i=1 a i )) = [{a 1 , . . . , a n }](∧ ⁿ _i=1 F a i )

(6)

f ^T (F (δ) ∨ [β]F (δ)) = f ^T (F (δ)) ∨ f ^T ([β]F (δ))

(7)

f ^T (C 1 ∧ C 2 ) = f ^T (C 1 ) ∧ f ^T (C 2 )

(8)

f ^T (C) = [any]f ^T (C)

(9)

f ^T (C ₁ U C ₂ ) = µZ.f ^T (C ₂ ) ∨ (f ^T (C ₁ ) ∧ [any]Z ∧ hanyi⊤)

(10)

f ^T ( C) = νZ.C ∧ [any]Z

(11)

f ^T ([& ⁿ _i=1 a i ]C) = [{a 1 , . . . , a n }]f ^T (C)

(12)

f ^T ([(& ⁿ _i=1 a i )α]C) = [{a 1 , . . . , a n }]f ^T ([α]C)

(13)

f ^T ([α + β]C) = f ^T ([α]C) ∧ f ^T ([β]C)

(14)

f ^T ([ϕ?]C) = f ^T (ϕ) ⇒ f ^T (C )

Table 1: The translation funtion

f ^T

^from

CL

^to

Cµ

^.

the formulaalsoholds in ase the set of states reahable by

p

^isempty.

We willnow translate the ve

CL

^lauses orresponding to the ontrat given above, into

Cµ

^{. Note that we use the}

^and

♦

^{with their lassial}

interpretation fromtemporallogis; the lastnot being inluded inthe Table

1. It isknown[BS01℄that

f ^T ( ♦ C) = f ^T (⊤UC) = µZ.C ∨ ([any]Z ∧ hanyi⊤)

^.

In order to translate the rst lause of the

CL

representation above we an proeed as follows:

f ^T ( F P (s) (f i)) = νZ.f ^T (F P (s) (f i)) ∧ [any]Z

^,

where:

f ^T (F P (s) (f i)) = f ^T (F (f i) ∧ [f i]P (s)) = [f i]F f i ∧ [f i]hsi¬F s .

In this manner, we use the

^{operator in the lauses below simply as}

syntati sugar (whih is redued to an expression using the

ν

^{operator in}

µ

^-alulus).

1.

[f i]F f i ∧ [f i]hsi¬F s

2.

[h](φ ⇒ (hpiO p ∧ h{d, n}i(O d ∧ O n )))

3.

[{d, n}](hliO l ∧ [l](µZ.h{p, p}iO p ∨ ([any]Z ∧ hanyi⊤)))

4.

[{d, n}][l](µZ.h{p, p, p}iO p ∨ ([any]Z ∧ hanyi⊤))

5.

[o]hsf DiO sf D

3.2 From

C µ

^{to the LTS}

In Fig. 2 wehave pitured one modelof the above lauseswhere we denote

by

else

^{all other ations dierent than the ones from the urrent node (e.g.}

for the state

s 7

^{inthe piture}

else = any \ {f i}

^).

Notethatbeauseofthesemantisofthe prohibition

F (f i)

^(i.e.,

[f i]F f i

^),

wewouldnotneedtoexpliitlyaddatransitionfromeahstatelabelledwith

f i

^{toastatewiththe}propositionalonstant

F f i

^{. However, inthepreseneof}

a CTP, asitis the asewith lause 1,weneed todosoin ordertorepresent

the reparation

P (s)

^.

WeattempttobuildamodelintheformofanLTSinaertainsensean

implementation of the ontrat as speied. The proess is done manually

and prone to error to ensure orretness of the automata we build, we

model hek them against the ontrat speiation. Furthermore, multiple

models satisfying the ontrat speiation exist, ranging from the weakest

being equivalent to the speiation itself, to stronger and more onrete

implementations. In this paper we are not onerned with ahieving the

weakest model.

GORDON,COULD YOU EXPAND ONTHIS?

Althoughtheweakestmodelisdesirabletohave,weanstillreasonabout

our ontrat based on a (orret) model we build. Given a model

M

^and

ontrat speiation

C

^{,we start oby provingthat the modelreallyimple-}

ments the ontrat:

M | = C

^{. We note that when the modeldoes not satisfy}

aproperty

π

^:

M 6| = π

^{, it}immediatelyfollowsthat neitherdoestheontrat:

C 6| = π

^{, thus enabling us to disover bugs in our speiation as translated}

fromthenaturallanguage,orintheoriginalnaturallanguageontrat itself.

On the other hand, using this approah, we annot prove the orretness of

the original ontrat. Were we able to obtain the weakest model, we would

have been able to reason diretlyabout the ontrat speiation itself.

In what follows, we will speify this model using the input language of

NuSMV, and provethat itis indeeda modelof the

CL

^formulae.

3.3 From the LTS to the NuSMV input syntax

GORDON: COULD YOU ADD AN EXPLANATION SOMEWHERE IN

THIS SECTION ON HOW WE ENCODED THEDYNAMIC DIAMOND?

I THINK IT COULD BE ALSO NICE TO EXPLAIN (HERE ORIN THE

CONCLUSION) ON WHY SIMPLY TAKING THE DUAL (BOX) DOES

NOT WORK PROBLEMS WITH THE INITIAL STATES?

InNuSMV[CCG

+

02℄,amodelanbespeiedintwoways: eitherusing

ation tehnique as it enables us to translate our system more diretly into

NuSMV.

NuSMVusesstatevariables toidentifystates;the numberofstatesisde-

termined bythe produtofthenumberofdierentvalueseahstatevariable

an take. There is alsoa seond kindof variables, input variables whih are

meanttospeifylabelsofalabelledtransitionsystem. Sinewehaveations

as labels, we make substantialuse of the input variablesin our appliation.

Wehave dened aninput variablefor eah atomiationofthe

CL

^spe-

iation. The type of the input variables is boolean so that if the value

of d = false then d is not an ative label of the transition. Whenever a

variableis left unspeied then NuSMV interprets itas having any value so

it reates atransition(or astate in ase of state variables)for eah value of

the variable.

InNuSMVitiseasytosimulatethe onurrent labels

{d, n}

^of

Cµ

^whih

mean that the transitionis taken if both ations

d

^and

n

^{are exeuted on-}

urrently: we ativate both input variables d = true ; n = true . We an

also represent the resoure-awareness of the labels (i.e. the

p&p

^of

CL

^{, or}

the

{p, p}

^of

C µ

^{) by dening the input variable with the type range of inte-}

gers. If p = 0 then the transitionis not labelled with the ation

p

^{; if p = 1}

then the transition is labelled with one normal ation

p

^{(like in the ase of}

boolean type); but if p = 2 then we take the transitionif two opies of the

ation

p

^{are exeuted} onurrently. We have then the following delaration of variables:

IVAR

d : boolean ;

n : boolean ;

p : 0 .. 3 ;

Notethatwe mayhaveempty transitions (withnolabel)by givingto all

the input variablesthe value false(orp = 0). Moreover, we mayrepresent

the speial ation

any

^of

Cµ

^{by leavingall input variablesunspeied.}

We have dened astate variablenamed state of enumeration type soit

an take onlyeightvalues, orrespondingtothe eightstatesdepited inFig.

2.

VAR

state : {s1,s2,s3,s4,s5,s6,s7,s8} ;

Other variables are delared aordingly (e.g., high : boolean). More-

over, wedeneastatevariableoftypeboolean foreahinput variable. This

is requiredby the

Cµ

^{where wehavea} propositionalonstant

O a

^or

F a

^asso-

iated toeahatomiation

a

^{whihenters underthe sopeof anobligation}

F_s : boolean ; F_fi : boolean ;

O_p : boolean ; O_d : boolean ; O_n : boolean ;

O_l : boolean ; O_sfD : boolean ;

As anexample, weshow below the enoding of the initialstate, and one

of its outgoing transitions, of the automaton in Fig. 2. We all the initial

state s1 .

INIT

(state = s1) & !high &

!F_fi & !O_p & !O_d & !O_n & !O_l & !O_sfD & !F_s ;

ThetransitionsarespeiedusingtheTRANSkeywordfollowedbyapropo-

sitionalformulawhihdeterminesthepairsof statesthatformthetransition

relation. The propositional formulaontains names of state variable (whih

are testedintheurrentstate)and nextexpressionswhihrefertothe value

of the state variables in the next state. It alsoontains the input variables

to model the labels of the transitions. Remember that any variable that is

missingfromtheformulaisinterpretedashavinganyvalue andwillgiverise

toanumberofdierenttransitionsequaltothenumberofvaluesitantake.

TRANS

--state variables of the urrent state

((state = s1) & !high &

!F_fi & !O_p & !O_d & !O_n & !O_l & !O_sfD & !F_s &

--input variables as the labels

(!fi & p = 0 & !d & !n & !l & !negl & !sfD & o & !s) &

--the values of the state variables in the next states

(next(state) = s6) & !next(high) &

next(!F_fi & !O_p & !O_d & !O_n & !O_l & !O_sfD & !F_s))

3.4 Model heking the Contrat

We propose to ombine the ontrat speiation and the model we build

in dierent ways with model heking tehniques to help us improve the

ontrat and inrease our ondene inour model.

Proving that the model satises the original lauses: Clearly, to

have ondene that we are reasoning using a orret model, we need to

prove that the automaton of Fig. 2, speied in NuSMV 2

respets the ve

2

TheNuSMVodewehaveusedisavailableonNordunet3projethomepage:

http://www.ifi.uio.no/~gerardo/nordunet3/software.shtml

CL

^lauses representing the statements from the ontrat example. For this we have speiedeah lause asa speial LTLspeiation in NuSMV:

3

G ((fi -> X F_fi) & (fi -> X (s & X !F_s)))

G(h -> X (high -> ( (an_p & (p=1 -> X O_p)) &

((an_dn & ((d & n) -> X (O_d & O_n)))))))

G((d&n) -> X( (an_l & (l -> X O_l)) &

(l -> X (F (an_pp & (p=2 -> X O_pp))))))

G((d&n) -> X(negl -> X(F(an_ppp & (p=3 -> X O_ppp)))))

G(o -> X(an_sfD & (sfD -> X O_sfD)))

As explained in the previous setion we have enoded the dynami dia-

mond in NuSMV by using the auxiliary variables an_a for eah ation a

inside a diamond.

Therst,seondandfourthpropertiesgothroughimmediately. Thethird

fails, but upon investigation, it turns out that the atual ontrat wording

gave a dependeny between the seond and third properties the

d&n

ation in the third property only refers to ones produed in the ontext of

the seond property (just after the Internet tra going high and the user

paying one). This indiates that the two ought to be ombined together

either by addingextra logi toindiatethe dependeny, orby mergingthen

into asingle property. We hoose the latter,obtaining:

4

G(h -> X (high -> ((an_p & (p=1 -> X O_p)) &

((an_dn & ((d & n) -> X (( (an_l & (l -> X O_l)) &

(l -> X (F (an_pp & (p=2 -> X O_pp))))) & O_d & O_n)))))))

This new property an beveried inour model.

Finally, the fth property fails, suggesting that our model is inorret.

However,uponinspetionitwasrealisedthatnothingintheontratspeies

that the ativationof the servie happens one,or thatthe user's obligation

is only valid the rst time the ativation ours. We hoose to revise the

originalontrat tostatethat: Thersttimetheservie beomesoperative,

the lient is obliged to send the Personal Data Form to Client Relations

Department. This is formulated as the following property, whih model

heks:

(!o) U (o -> X(an_sfD & (sfD -> X O_sfD)))

Analternativesolutionistoensurethattheontratisonlyinforeone

the Internet Servie beomes operative, and simplify the property aord-

ingly.

3

TheNuSMVodepresentedin[PPS07℄isinorret.

4

TheNuSMVodepresentedin[PPS07℄isinorret.

property we want to hek on the ontrat model an be expressed in En-

glish as: It is always the ase that whenever the Internet tra is high,

if the lients pays immediately, then the lient is not obliged to pay again

immediately afterwards. The property is expressed in

CL

^{-like syntax5 as:}

(φ ⇒ [p]¬O(p))

^{.6 The property proves to be false, as an be seen in the}

transript below, whihinludes aounter-example:

NuSMV > hek_ltlspe

-- speifiation

G (!high | (p = 1 -> X (p = 1 -> X !O_p))) is false

-- as demonstrated by the following exeution sequene

-> State: 2.1 <-

state = s1; o = 1

-> State: 2.2 <-

state = s2; sfD = 1

-> State: 2.3 <-

state = s3; O_p = 1; O_sfD = 1; h = 1

-- Loop starts here

-> State: 2.4 <-

state = s4; high = 1; O_sfD = 0; p = 1

-- Loop starts here

-> State: 2.5 <-

p = 1

The above ounter-example shows that in state s4 of Fig. 2 the lient

must fulloneofthefollowingobligations: ortopay(p),ortodelaypayment

andnotify(d ,n). However,afterpayingone,theautomatonisstillinastate

with high tra (state s4), and thus the lientis stillobliged topay again.

We give in Fig. 3-athe new model, whihis proved orret with respet

to the above property. The dierene is the transition

s 4

−→ p s 3

^whih

replaes the one labelled with

p

^from

s ₄

^{to itself. From this it is easy now}

to modify the original ontrat by introduing the following lause: The

provider guarantees that if the Internet tra of the Client reahes a high

level and the Client pays the [prie℄ then it will not be obliged to pay the

[prie℄ again.

Notiethatthoughwehaveobtainedanewmodelthatsatisestheprop-

erty (and a lause in the original ontrat solving the above problem), the

solution is still not satisfatory, as the ontrat does not speify what hap-

pens after the lient pays but does not derease the Internet tra. In the

newmodelshown inFig. 3-athisisreetedbythefatthataftertakingthe

5

Notiethatformally in

CL

^{thereisnonegationatthelause level.}

6

Note that NuSMV, in ontrast with for instane SPIN, aepts the formula in its

positiveformulationandthus itisnotneededto negateitbeforefeedingitinto thetool.

Thisformulainorretlyappearsin[PPS07℄as

¬(φ ⇒ [p]¬O(p))

^.

the Internettraislow. Forbrevity wedonotfurtheranalyse theontrat

in order toobtain the right ontrat onerning this problem,thoughit an

bedone followinga similarapproah as above.

Verifying a property about payment in ase of inreasing Internet

tra: The heking of the previous property was done for the benet of

thelient. Wenowperformmodelhekinginordertoinreasetheondene

of the provider of the servie.

Weareinterestedinprovingthat: ItisalwaystheasethatwheneverIn-

ternettraishigh,ifthelientdelayspaymentandnoties,andafterwards

lowers the Internet tra, then the lient is forbidden to inrease Internet

tra until he pays twie the prie. This ompliated English lause is

speied in

CL

^{-like syntax as:}

(φ ⇒ [d&n · l](F (h) U

^done

p&p ))

^.

Here done

p&p

^{is anassertionadded tospeify that the lient has paid twie.}

Notie that in order to prove the property we need to extend the NuSMV

modeloftheontratwithapropositionalonstantorrespondingtodone

p&p

whihis true only aftera transitionlabelled

{p, p}

^{is taken.}

InFig. 3-aweshowtheontrolstrutureoftheLTS.Theadditionalstate

variabledone

p&p

^{isadded tothe NuSMVmodel,thus eetivelyintroduing}

twostatesforeveryoneinFig. 3-a,withdierentvaluesforthestatevariable.

The original property proves to be false, sine from state

s 4

^(where

φ

holds), after

d&n · l

^{, itis possibleto inrease Internet trainstate}

s ₇

^(due

to the

else

^{label), so neither}

F (h)

^{nor done}

p&p

^hold.

Though it was not apparent at rst sight, and onrmed by the result

givenby thetool,theabovelauseallowthe lienttogofromnormaltohigh

Internet tramany times and pay the penalty (

2 ∗ [price]

^{) onlyone. The}

problemisthatafterthelientlowers theInternettra,hemightgetahigh

tra again and postpone the payment till a future moment. This problem

omes from the ambiguity of the language. Note that the

CL

formalisation inthe lauses3 and4 usethe

♦

^{tomodelthe fatthat astatementwillhold}

eventually in the future but not neessarily immediately (expressions pay

later in lause 7.3and willhaveto pay in lause7.4 are the ambiguities).

Theeventuallywastranslatedwiththehelpofthespeialsyntax

else

^thatwe

see in Fig. 3-a. We use the ounter-example given by NuSMV to onstrut

the model in Fig. 3-b where the property holds. The dierene is at the

transition from

s 7

^to

s 3

^{where we have hanged the label to the multi-set}

label

{p, p}

^{. In}

CL

^{the solution is to add a new lause} orresponding to the property above, and the original ontrat should be extended with the

English version of the property as expressed above. Note that a similar

in Fig. 3-b alsoby replaing the label of the transitionfrom

s 6

^to

s 3

^{by the}

multi-set label

{p, p, p}

^.

4 Final Disussion

Inthispaperwehaveshown howmodelhekingtehniquesandtoolsanbe

appliedto analyseontrats. Inpartiular,wehaveused NuSMV[CCG

+

02℄

to model hek onventional ontrats speied using the language

CL

^{, and}

we have presented multiple uses of modelheking for reasoning about on-

trats. Firstly, we use model heking to inrease our ondene in the

orretness of the model with respet to the original natural language on-

trat. Seondly, by ndingerrors in the model, we identify problems in the

originalnaturallanguageontratoritsinterpretationin

CL

^{. Finally,ween-}

able the signatoriestosafeguard theirinterests by ensuring ertaindesirable

properties hold (and ertainundesirable ones do not).

AboutNuSMV: NuSMV[CCG

+

02℄isthesuessorofthemilestonesym-

bolimodel heker SMV [MM93 ℄. Symboli modelheking [BCM

+

90℄ is

based onthe lever enoding of the states usingbinary deision diagramsor

similar tehniques, but stillrelies onthe lassial modelheking algorithm.

NuSMV allows the heking of properties speied in CTL, LTL, or PSL.

More reentlyNuSMV has inluded input variables withwhihit ispossible

to speify diretly labelled transition systems. This feature of NuSMV has

been very useful inour ontext.

Related Work: To our knowledge, model heking ontrats is quite an

unexplored area where only few works an be found [SMJS03, Das00 ℄. The

main dierene with our approah is that in [SMJS03 ℄ there is no language

for writing ontrats, insteadautomata are used to modelthe dierent par-

tiipants of a ontrat, i.e. there is no model of the ontrat itself but only

of the behaviour of the ontrat signatories. Many safety and liveness prop-

erties identied as ommonto e-ontrats are then veried in a purhaser/-

supplier ase study using SPIN [Hol03℄. Similarly,in [Das00℄ Petri nets are

used to model the behaviour of the partiipants of a ontratual protool.

Though in[SMJS03℄ it is laimedthat modellingthe signatories gives mod-

ularity, adding lauses to a given ontrat implies modifyingthe automata.

In our ase, adding lauses to a ontrat is done as in any delarative lan-

guage, without hanging the rest. Though in our urrent implementation

we would also need to rewrite the veriation model, this should not be

seen asa disadvantage; given that

CL

^{has formalsemantis in}

C µ

^{the model}

our approah is the possibility of expliitly writing onditional obligations,

permissionsand prohibitions,as wellasCTDs and CTPs. We arenot aware

of anyotherwork onmodelhekinge-ontrats alongthesame lineasours.

See[PS07 ℄and[SMJS03 ℄(andreferenestherein)forfurtherdisussions,and

other approahes, on formalisationsof ontrats.

Future Work: The approah we have followed has few drawbaks. First

notie thatthe way wehaveobtained themodelforthe least x-pointinthe

C µ

^{formula3 in Setion3.1 was modelledas the yle}

(s 7 , s 3 , s 4 , s 5 ) ^∗

^{, whih}

may indeed be an innite loop as we do not have aepting onditions in

our labelled Kripke struture nor fairness onstraints. This of ourse would

need tobe rened inorder toguarantee that the yle willeventuallynish.

Moreover, inorder to be able toprove properties about ations whihmust

have been performed, we should extend our language with a onstrutor

done(·)

^{to be applied to ations, meaning that the ation argument was}

performed(aswiththedone

p&p

^{intheexample). Thiswilldenitelyfailitate}

speifying properties like the lastone of the previous setion onerning the

prohibition onationsby the lient. Weare urrently working onimproving

the aboveaspets in order tomake a more preiseanalysis.

We have presented a manual translation from the

Cµ

^{semantis of the}

ontrat written in

CL

^{into the input language of NuSMV. We plan to im-}

plement a tool to automatially model hek ontrats written in

CL

^{. We}

an benet fromtheounter-example generationtox theoriginalontrat,

as we have briey shown in Setion 3.4. Although we use NuSMV as the

underlying modelheker we plan tomoveon toa

µ

^{-alulusmodelheker}

(e.g., [Bie97, MS03℄).

With suh a tool the whole model heking proess will be aelerated

failitatingitsuse andthusmaking iteasytoproveother interesting general

propertiesaboute-ontrats,assuggestedin[SMJS03℄. Besidessuhlassial

livenessorsafetypropertiesweare alsointerestedinpropertiesmorespei

toe-ontrats,inluding: ndingtheobligationsorprohibitionsofone ofthe

parties in the ontrat; listingof allthe rights that followafter the fullling

of anobligation;whatare the penaltiesfor wheneverviolating anobligation

orprohibition;determiningwhether agivenpartiipantisobligedtoperform

ontraditory ations.

Thegenerationof the (automata-like)modelthat wedid by handinSe-

tion 3 an be done automatially along the lines of existing LTL-to-Bühi

automata translators (like ltl2smv or ltl2ba). [RV07℄ presents a ompre-

hensive overview of the state-of-the-art of suh tools.

In the urrent state of development, the language

CL

^{annot expliitly}

ing the language with real-time features in order to be able to speify and

verify time-dependant properties.

Aknowledgements. WewouldliketothankMartinSteenforsuggestions

on anearlydraft of this paper

Referenes

[BCM

+

90℄ Jerry R. Burh, Edmund M. Clarke, Kenneth L. MMillan,

David L. Dill, and L. J. Hwang. Symbolimodel heking: 10

20

states and beyond. In LICS'90,pages 428439.IEEE Computer

Soiety, 1990.

[Bie97℄ A. Biere. mu-ke - eient mu-alulus model heking. In

CAV'97, volume 1254 of LNCS, pages 468471,1997.

[BS01℄ JulianBradeldandColinStirling.ModalLogisandMu-Caluli:

an Introdution, pages293330. Elsevier, 2001.

[CCG

+

02℄ A. Cimatti, E. Clarke, E. Giunhiglia, F. Giunhiglia, M. Pis-

tore, M. Roveri, R. Sebastiani, and A. Tahella. NuSMV 2: An

OpenSoure Tool for Symboli Model Cheking. In CAV 2002,

volume 2404 of LNCS, pages 359364.Springer, 2002.

[Das00℄ Aspassia Daskalopulu. Modelheking ontratualprotools. In

JURIX'00, Frontiers in Artiial Intelligene and Appliations

Series, pages 3547.IOS Press, 2000.

[FL77℄ Mihael J. Fisher and Rihard E. Ladner. Propositional modal

logi of programs. In STOC'77, pages286294. ACM, 1977.

[Hol03℄ G.J.Holzmann. The Spin Model Cheker, Primerand Referene

Manual. Addison-Wesley, Reading, Massahusetts, 2003.

[Koz83℄ Dexter Kozen. Resultson the propositionalmu-alulus. Theor.

Comput. Si.,27:333354, 1983.

[MM93℄ Kenneth L. MMillan. Symboli Model Cheking. Kluwer Aa-

demi Publishers, 1993.

[MN06℄ Paul MNamara. Deonti logi. volume 7 of Handbook of the

History ofLogi, pages197289.North-HollandPublishing,2006.

model-heking for regular alternation-free mu-alulus. Si.

Comput. Program.,46(3):255281,2003.

[Pnu77℄ AmirPnueli. Thetemporallogiofprograms. InFOCS'77,pages

4657. IEEE Computer Soiety Press, 1977.

[PPS07℄ GordonPae,CristianPrisaariu,andGerardoShneider. Model

heking ontrats a ase study. In 5th International Sym-

posium on Automated Tehnology for Veriation and Analysis

(ATVA'07), volume 4762 of LNCS, pages 8297, Tokyo, Japan,

Otober2007. Springer-Verlag.

[PS07℄ Cristian Prisaariu and Gerardo Shneider. A formal language

for eletroni ontrats. In FMOODS'07,volume 4468 of LNCS,

pages 174189.Springer, 2007.

[RV07℄ Kristin Y. Rozier and Moshe Y. Vardi. Ltl satisability hek-

ing. InDragan Bosnaki andStefan Edelkamp, editors,SPIN'07,

volume 4595 of LNCS, pages 182200.Springer-Verlag,2007.

[SMJS03℄ Ellis Solaiman,Carlos Molina-Jiménez, and Santosh K. Shrivas-

tava. Model heking orretness properties of eletroni on-

trats. InICSOC'03,volume2910ofLNCS,pages303318,2003.

1. [name℄,fromnowonreferredtoasProviderand

2. [name℄,fromnowonreferredtoastheClient.

INTRODUCTION

3. TheProviderisobligedtoprovidetheInternetServiesasstipulatedinthisAgreement.

5. DEFINITIONS

5.1. j) InternettramaybemeasuredbybothClientandProviderbymeansofEquipment

andmaytakethetwovalueshighandnormal.

OPERATIVE PART

7. CLIENT'SRESPONSIBILITIESANDDUTIES

7.1. TheClientshallnot:

a) supplyfalseinformationtotheClientRelationsDepartmentoftheProvider.

7.2. Whenever theInternetTra ishighthen theClientmustpay

[price]

immediately,orthe ClientmustnotifytheProviderbysendingane-mailspeifyingthathewillpaylater.

7.3. IftheClientdelaysthepaymentasstipulatedin7.2,afternotiationhemustimmediately

lowertheInternettratothenormallevel,andpaylatertwie(

2 ∗ [price]

^).

7.4. IftheClientdoesnotlowertheInternettraimmediately,thentheClientwillhavetopay

3 ∗ [price]

^.

7.5. The Clientshall, as soon as the Internet Servie beomesoperative, submit within seven

(7)daysthe PersonalDataFormfromhisaounton the Provider'swebpageto theClient

RelationsDepartmentoftheProvider.

8. CLIENT'SRIGHTS

8.1. TheClientmayhoosetopayeither:

a)eahmonth; b)eahthree(3)months; )eahsix(6)months;

9. PROVIDER'SSERVICE

9.2. AspartoftheServieoeredbytheProvidertheClienthastherighttoane-mailandan

useraount.

9.3. Providerisobligedtooerwithnolimitationandwithinaperiodofseven(7)daysapassword

andanyotherEquipmentSpeitoClient,neessaryfortheorretusageoftheuseraount,

uponreeivingofalltheneessarydataaboutthelientfromtheClientRelationsDepartment

oftheProvider.

9.4. Eahmonththe Clientpaysthe bill the Providerisobliged tosendaReportofInternet

UsagetotheClient.

10. PROVIDER'SDUTIES

10.1. TheProvidertakesthe obligationtoreturnthe personaldataofthelienttotheoriginal

statusupon terminationofthe presentAgreement,and afterwards todelete andnot usefor

anypurposeanywholeorpartofit.

10.2. TheProviderguaranteesthattheClientRelationsDepartment,aspartofhisadministrative

organisation, willberesponsive to requestsfromthe Clientor any otherDepartmentof the

Provider,ortheProvideritselfwithinaperiodlessthantwo(2)hoursduringworkinghours

orthedayafter.

11. PROVIDER'SRIGHTS

11.1. TheProvidertakestherighttoalter,delete,orusethepersonaldata ofthe Clientonly

forstatistis,monitoringandinternalusageintheondeneoftheProvider.

11.2. Providermay,atitssoledisretion, withoutnotieorgivinganyreason orinurringany

liabilityfordoingso:

b) SuspendInternetServiesimmediatelyifClientisinbreahofClause7.1;

13. TERMINATION

13.1. Without limiting the generality of any other Clause inthis Agreement the Clientmay

terminate thisAgreement immediately withoutanynotie and beingvindiated ofany ofthe

ClauseofthepresentAgreementif:

a) theProviderdoesnotprovidetheInternetServieforseven(7)daysonseutively.

13.2. The Providerisforbidden to terminate the present Agreement without previous written

notiationbynormalpostandbye-mail.

13.3. TheProvidermayterminatethepresentAgreementif:

a) anypaymentduefromClienttoProviderpursuanttothisAgreementremainsunpaidfor

aperiodoffourteen(14)days;

16. GOVERNINGLAW

16.1. TheProviderandthepresentAgreementaregovernedbyandonstruedaordingtothe

LawRegulatingInternetServiesandtotheLawoftheState.

a) TheLawoftheStatestipulatesthatanyISPProviderisobliged,uponrequesttoseizeany

ativityuntilfurthernotiefromtheStaterepresentatives.

F _s

¬

F _fi

O _l O _sfD , O _p

O _d , O _n φ ^, O _p l −

sfD o

l s

fi {d,n}

fi p h

fi fi fi fi

fi

else else

s3

s5 s4 s6 s7 s8

s1

s2

Figure2: Example of a modelfor the velauses written in

CL

^.

F _s

¬

F _fi

O _l O _sfD , O _p l −

F _s

¬

F _fi

O _l O _sfD , O _p l −

O _d , O _n O _d , O _n

sfD o

l s

fi {d,n}

fi h

fi fi fi fi

fi

s3

s5 s4 s6 s7 s8

s1

s2

sfD o

l s

fi {d,n}

fi h

fi fi fi fi

fi

else else

s3

s5 s4 s6 s7 s8

s1

s2

a. b.

p p

φ φ

{p,p,p}

{p,p}

Figure 3: The model ofFig. 2 orreted.