1

11

Corso di Laurea MagistraleCorso di Laurea Magistralein in

Ingegneria InformaticaIngegneria Informaticaper la Gestione dper la Gestione d’’aziendaaziendaGestione della Qualità-II parte

La produzione del software: metodologie estandards

a.a.a.a. 20102010--20112011Docente: Gigliola Docente: Gigliola VagliniVaglini

22

LessonsLessons 9,109,10

Software Engineering Tools and Software Engineering Tools and MethodsMethods

2

33

Software Software engineeringengineering toolstools Software Software developmentdevelopment toolstools are the are the computercomputer--

basedbased toolstools thatthat are are intendedintended toto assist the assist the software life software life cyclecycle processesprocesses..

ToolsTools allowallow wellwell--defineddefined actionsactions toto bebeautomatedautomated. .

ToolsTools are are oftenoften designeddesigned toto supportsupport particularparticularsoftware software engineeringengineering methodsmethods. .

LikeLike software software engineeringengineering methodsmethods, , theythey are are intendedintended toto makemake software software engineeringengineering more more systematicsystematic, and , and theythey varyvary in scope in scope fromfromsupportingsupporting individualindividual taskstasks toto encompassingencompassing the the complete life complete life cyclecycle..

44

Software Software RequirementsRequirements ToolsTools ToolsTools forfor dealingdealing withwith software software requirementsrequirements

havehave beenbeen classifiedclassified intointo twotwo categoriescategories: : modelingmodeling and and traceabilitytraceability toolstools..–– RequirementsRequirements modelingmodeling toolstools are are usedused forfor elicitingeliciting, ,

analyzinganalyzing, , specifyingspecifying, and , and validatingvalidating software software requirementsrequirements

–– RequirementRequirement traceabilitytraceability toolstools are are becomingbecomingincreasinglyincreasingly importantimportant asas the the complexitycomplexity ofof software software growsgrows. . SinceSince theythey are are alsoalso relevantrelevant in in otherother life life cyclecycleprocessesprocesses, , theythey are are presentedpresented separatelyseparately fromfrom the the requirementsrequirements modelingmodeling toolstools..

3

55

Software Design and Software Design and ConstructionConstructionToolsTools

The first topic covers tools for creating and checking software designs.

The second topic covers tools used to produce and translate program representation (forinstance, source code) which is sufficientlydetailed and explicit to enable machineexecution. Examples are– Program editors.– Compilers and code generators.– Interpreters.– Debuggers.

66

Software Software TestingTesting ToolsTools Test generators that assist in the development of test

cases. Test execution frameworks that enable the execution

of test cases in a controlled environment. Test evaluation tools that support the assessment of

the results of test execution, helping to determinewhether or not the observed behavior conforms to the expected behavior.

Test management tools that provide support for allaspects of the software testing process.

Performance analysis tools that are used for measuringand analyzing software performance.

4

77

Software Software MaintenanceMaintenance ToolsTools

TwoTwo categoriescategories are are identifiedidentified::–– ComprehensionComprehension toolstools thatthat assist in the assist in the humanhuman

comprehensioncomprehension ofof programsprograms. . ExamplesExamples include include visualizationvisualization toolstools suchsuch asas animatorsanimators..

–– ReengineeringReengineering toolstools. . ReengineeringReengineering isis defineddefined asas the the examinationexamination and and alterationalteration ofof a software a software productproduct totoreconstitutereconstitute itit in a in a newnew formform, and , and includesincludes the the subsequentsubsequent implementationimplementation ofof the the newnew formform. . ReengineeringReengineering toolstools supportsupport thatthat activityactivity.. Reverse Reverse engineeringengineering toolstools assist the assist the processprocess byby workingworking

backwardsbackwards fromfrom anan existingexisting productproduct toto create create artifactsartifacts suchsuchasas specificationspecification and design and design descriptionsdescriptions, , whichwhich thenthen can can bebetransformedtransformed toto generate a generate a newnew productproduct fromfrom anan oldold oneone..

88

Software Software EngineeringEngineering Management Management ToolsTools

Software Software engineeringengineering management management toolstoolsare are subdividedsubdivided intointo threethree categoriescategories: : project planning and project planning and trackingtracking, , riskriskmanagement, and management, and measurementmeasurement..–– Project planning and Project planning and trackingtracking toolstools are are usedused

in in efforteffort measurementmeasurement and and costcost estimationestimation..–– RiskRisk management management toolstools are are usedused in in

identifyingidentifying, , estimatingestimating, and , and monitoringmonitoring risksrisks..–– MeasurementMeasurement toolstools assist in assist in performingperforming the the

activitiesactivities relatedrelated toto the software the software measurementmeasurement programprogram..

5

99

Software Software EngineeringEngineering ProcessProcess ToolsTools Software Software engineeringengineering processprocess toolstools are are divideddivided

intointo modelingmodeling toolstools, management , management toolstools, and , and software software developmentdevelopment environmentsenvironments..–– ProcessProcess modelingmodeling toolstools modelmodel and investigate and investigate

software software engineeringengineering processesprocesses..–– ProcessProcess management management toolstools provideprovide supportsupport forfor

software software engineeringengineering management.management.–– Software Software developmentdevelopment environmentsenvironments..

IntegratedIntegrated computercomputer--aidedaided software software engineeringengineering toolstools or or environmentsenvironments cover multiple cover multiple phasesphases ofof the software the software engineeringengineering life life cyclecycle. . SuchSuch toolstools performperform multiple multiple functionsfunctionsand and potentiallypotentially interactinteract withwith the software life the software life cyclecycle processprocessbeingbeing executedexecuted..

ProcessProcess--centeredcentered software software engineeringengineering environmentsenvironments explicitlyexplicitlyincorporate information on the software life incorporate information on the software life cyclecycle processesprocesses and and guide and monitor the guide and monitor the useruser accordingaccording toto the the defineddefined processprocess..

1010

Software Software QualityQuality ToolsTools QualityQuality toolstools are are divideddivided intointo twotwo

categoriescategories: : inspectioninspection and and analysisanalysis toolstools..–– ReviewReview and and auditaudit toolstools. . TheseThese toolstools are are usedused

toto supportsupport reviewsreviews and and auditsaudits..–– StaticStatic analysisanalysis toolstools. . TheseThese toolstools are are usedused toto

analyzeanalyze software software artifactsartifacts, , suchsuch asas syntacticsyntacticand and semanticsemantic analyzersanalyzers, , asas wellwell asas data, data, controlcontrol flow, and flow, and dependencydependency analyzersanalyzers. . SuchSuchtoolstools are are intendedintended forfor checkingchecking software software artifactsartifacts forfor conformanceconformance or or forfor verifyingverifyingdesireddesired propertiesproperties..

6

1111

Software Software engineeringengineering methodsmethods Software Software engineeringengineering methodsmethods impose impose

structurestructure on the software on the software engineeringengineering activityactivitywithwith the goal the goal ofof makingmaking the the activityactivity systematicsystematicand and ultimatelyultimately more more likelylikely toto bebe successfulsuccessful. .

MethodsMethods usuallyusually provideprovide a a notationnotation, , proceduresproceduresforfor performingperforming identifiableidentifiable taskstasks, and , and guidelinesguidelines forfor checkingchecking bothboth the the processprocess and and the the productproduct. .

TheyThey varyvary widelywidely in scope, in scope, fromfrom a single life a single life cyclecycle phasephase toto the complete life the complete life cyclecycle. . WeWeconsiderconsider herehere methodsmethods encompassingencompassing multiple multiple life life cyclecycle phasesphases..

1212

Software Software EngineeringEngineering MethodsMethods

The The Software Software EngineeringEngineering MethodsMethods subareasubarea isisdivideddivided intointo threethree topicstopics: : –– heuristicheuristic methodsmethods dealingdealing withwith informalinformal approachesapproaches, , –– prototypingprototyping methodsmethods dealingdealing withwith software software

engineeringengineering approachesapproaches basedbased on on variousvarious formsforms ofofprototypingprototyping, and, and

–– formalformal methodsmethods dealingdealing withwith mathematicallymathematically basedbasedapproachesapproaches

7

1313

The The threethree topicstopics are are notnot disjointdisjoint; ; ratherrathertheythey representrepresent distinctdistinct concernsconcerns. . ForForexampleexample, , anan objectobject--orientedoriented methodmethod maymayincorporate incorporate formalformal techniquestechniques and and relyrely on on prototypingprototyping forfor verificationverification and and validationvalidation..

1414

HeuristicHeuristic methodsmethods

ThisThis topictopic containscontains some some categoriescategories: : structuredstructured, , datadata--orientedoriented, and , and domaindomain--specificspecific. . –– The The domaindomain--specificspecific categorycategory includesincludes specializedspecialized

methodsmethods forfor developingdeveloping systemssystems whichwhich involve realinvolve real--time, time, safetysafety, or security , or security aspectsaspects..

–– WhenWhen usingusing structuredstructured methodsmethods the system the system isis builtbuiltfromfrom a a functionalfunctional viewpointviewpoint, , startingstarting withwith a a highhigh--levellevelviewview and and progressivelyprogressively refiningrefining thisthis intointo a more a more detaileddetailed design.design.

–– DataData--orientedoriented methodsmethods are are usedused whenwhen the the mainmain part part ofof the system the system isis the data the data structuresstructures thatthat a a programprogrammanipulatesmanipulates ratherrather thanthan the the functionfunction itit performsperforms..

8

1515

PrototypingPrototyping MethodsMethods

WhenWhen dealingdealing withwith software software prototypingprototypingwewe mustmust definedefine–– the the prototypingprototyping style, i.e. the style, i.e. the approachapproach toto bebe

followedfollowed: : throwawaythrowaway, , evolutionaryevolutionary, and , and executableexecutable specificationspecification..

–– the the prototypingprototyping target, target, forfor exampleexamplerequirementsrequirements specificationspecification, , architecturalarchitecturaldesign, or the design, or the useruser interface.interface.

–– the the prototypingprototyping evaluationevaluation techniquestechniques, i.e. the , i.e. the way in way in whichwhich the the resultsresults ofof a a prototypeprototypeexerciseexercise are are usedused..

1616

FormalFormal MethodsMethods

VariousVarious aspectsaspects ofof formalformal methodsmethods can can bebepointedpointed outout–– SpecificationSpecification languageslanguages and and notationsnotations, i.e., the , i.e., the

specificationspecification notationnotation or or languagelanguage usedused; ; specificationspecificationlanguageslanguages can can bebe, , forfor exampleexample, , propertyproperty--orientedoriented, or , or behaviorbehavior--orientedoriented..

–– The way in The way in whichwhich the the methodmethod refinesrefines (or (or transformstransforms) ) the the specificationspecification intointo a a formform whichwhich isis closercloser toto the the desireddesired finalfinal formform ofof anan executableexecutable programprogram..

–– VerificationVerification//provingproving propertiesproperties, i.e., the way in , i.e., the way in whichwhichthe system the system propertiesproperties are are provedproved, , forfor exampleexamplethroughthrough modelmodel checkingchecking..

9

1717

Specification and verificationSpecification and verification

The concurrent systems caseThe concurrent systems case

1818

•

System System specificationspecification

The description of the system is The description of the system is abstracted from abstracted from implementativeimplementative details details but it must be:but it must be:

comprehensiblecomprehensible unambiguousunambiguous expressiveexpressive

A A formalformal system system specificationspecification isis writtenwrittenin a in a rigorousrigorous languagelanguage and and isis basedbased on a on a sound sound theorytheory

10

1919

FormalFormal methodsmethods FormalFormal methodsmethods are are mathematicalmathematical approachesapproaches

toto solvingsolving software (and hardware) software (and hardware) problemsproblems at at the the requirementsrequirements, , specificationspecification and design and design levelslevels. .

VariousVarious formalformal specificationspecification notationsnotations are are availableavailable, in , in particularparticular Finite State Finite State MachineMachinebasedbased methodologiesmethodologies allowallow executableexecutable software software specificationspecification ..

FormalFormal methodsmethods are are mostmost likelylikely toto bebe appliedappliedparticularlyparticularly wherewhere the software the software isis safetysafetycriticalcritical. Software . Software safetysafety assuranceassurance standardsstandardsdemanddemand formalformal methodsmethods..

2020

System VerificationSystem Verification

DoesDoes the system the system respectrespect a a givengivenpropertyproperty??–– The property can be verified on the system The property can be verified on the system

specificationspecification–– The verification can be carried on in an The verification can be carried on in an

automatic way in the verification environment automatic way in the verification environment –– The The verificationverification can can bebe formalformal, i.e., , i.e., Properties are formally defined Properties are formally defined Proofs are Proofs are rigourousrigourous

11

2121

•

Concurrent SystemsConcurrent Systems

ConcurrentConcurrent systemssystems are are characterizedcharacterized bybythe the existenceexistence ofof

–– Parallel eventsParallel events–– Communicating eventsCommunicating events–– Nondeterministic occurrence of eventsNondeterministic occurrence of events

2222

P1: R=R+1;P2: R=R*2; P1|| P2

The program result depends on the relative speed of the concurrent activities

The functional semantics (input/output) of the sequential languages is not suitable

P1 P2R

ParallelismParallelism

12

2323

• A new kind of semantics is given to concurrent programsbased on automata theory :• machine state• state transition (an action\event can cause

a state transition)• program semantics= state machine

y:3y =y+1;

y:4

Operational semanticsOperational semantics

2424

SemanticSemantic descriptiondescription ofofconcurrencyconcurrency

InterleavingInterleaving–– The The concurrentconcurrent executionexecution ofof actionaction aa and and

actionaction bb producesproduces anan effecteffect equivalentequivalent toto anyanysequentialsequential executionexecution ofof a and b, i.e. a and b, i.e. abab or or baba

TrueTrue concurrecyconcurrecy–– The The concurrentconcurrent executionexecution ofof actionaction a and a and

actionaction b can produce b can produce anan effecteffect equivalentequivalentneitherneither toto abab nornor toto baba

13

2525

R:1 R:2

R:3

R:2

R:4

P2

P1

P2P1

P1: R=R+1; P2: R=R*2;

P1|| P2

InterleavingInterleaving semanticssemantics

2626

R:1 R:2

R:2

P2

P1

P1: R=R+1; P2: R=R*2;

P1|| P2

TrueTrue concurrencyconcurrency semanticssemantics

14

2727

SpecificationSpecification languageslanguages Algebraic languagesAlgebraic languages

–– Algebra = data + operators on dataAlgebra = data + operators on data

ProcessProcess algebraalgebra–– Data=processesData=processes–– Operators=Operators= parallelparallel compositioncomposition, ,

nondeterministicnondeterministic choicechoice, , communicationcommunication……

2828

CalculusCalculus of of CommunicatingCommunicatingSystemsSystems (CCS) ((CCS) (MilnerMilner ‘‘89)89)

StructuralStructural operationaloperational semanticssemantics (SOS)(SOS) ConcurrencyConcurrency asas interleavinginterleaving SinchronousSinchronous communicationcommunication SeveralSeveral processprocess equivalencesequivalences are are

defineddefined

15

2929

ModelModel checkingchecking

PropertiesProperties verificationverification throughthrough modelmodelcheckingchecking

Si verificano proprietSi verificano proprietàà della specifica su della specifica su una struttura (sistema a stati finiti) che una struttura (sistema a stati finiti) che èèla sua semanticala sua semantica La verifica avviene tramite un algoritmo, La verifica avviene tramite un algoritmo,

non con non con theoremtheorem provingproving

3030

ModelModel checkingchecking vs vs TheoremTheoremprovingproving

MC MC isis semanticssemantics basedbased: si : si viaggia sulla struttura e viaggia sulla struttura e in ogni stato deve essere in ogni stato deve essere soddisfatta una soddisfatta una sottoproprietsottoproprietàà

Per proprietPer proprietàà non non ricorsive la complessitricorsive la complessitààdegli algoritmi esistenti degli algoritmi esistenti èèlineare (lineare (n+mn+m))

TP TP isis syntaxsyntax basedbased: si : si cercano di costruire tutti cercano di costruire tutti i programmi che hanno i programmi che hanno una certa proprietuna certa proprietàà..

La strategia La strategia èè fornita fornita dalldall’’utente (non utente (non automatizzabile)automatizzabile)

Ci sono infiniti programmi Ci sono infiniti programmi che hanno la proprietche hanno la proprietààvolutavoluta…………

16

3131

P ::= nil | .P | P+P | P|P | P\L | P[f] | C

A = {a, b, .. } input actions

Vis = A ‘A observable actions non observable action

Act = Vis U {} action alphabet

‘A = {‘a, ‘b .. } output actions

C := P process definition

L Vis f : Act Act

CCS CCS syntaxsyntax

3232

Outputchannels

Inputchannels

P‘a

‘b

c

d..

.

.

ProcessProcess interfaceinterface

17

3333

Each process P is associated with a labeledtransition system, LTS(P), that defines the behavior of P

• states = process• initial state = P• labels Act

CCS CCS semanticssemantics

3434

P := a.b.P + c. (a.d.P + c.’e.Q)Q := c.Q + ‘b.P

ab

a

‘e

c

d

c

‘bc

P

LTS(P)

ExampleExample

18

3535

• it is defined by structural induction on the syntax• inference rules are used to define the transitionrelation

premiseconclusion

StructuralStructural operationaloperationalsemanticssemantics ofof CCSCCS

3636

nil • no action is executed• no inference rule is needed• this constant expresses the process termination

(success or failure/deadlock)

.P • the prefix of the term is an action• no premise needs• it expresses the sequentiality: the action

a is executed and after the behavior of P is followed

.P P act

SOSSOSCCSCCS

19

3737

a b

LTS(a.b.nil)

a.b.nil b.nil nila.b.nilba

((contcont.).)

a.b.nil b.nila

act

Proof of the transition:It exists a sequence of rule applicationsthat leads from a.b.nil to b.nil

a.b.nil b.nila

3838

sum_1P P’

P+ Q P’

sum_2P+ Q Q’

Q Q’

sum_1

P + Q • this process can behave as P or as Q• the choice is non deterministic• the operator + is associative

NondeterministicNondeterministic choicechoice

20

3939

a

a.nil + b.nilba

ba.nil+b.nil nil

((contcont.).)

a.nil + b.nil nila

a.nil nila

act

sum_1

Proof of the transition a.nil + b.nil nila

4040

c. ( a.nil + b.nil ) ca b

a

ba.nil+b.nil nilc.(a.nil+b.nil)

c

LTS(c.(a.nil+b.nil))

((contcont.).)

21

4141

X P’con

P P’if X:= P

X • process name or constant definition• it expresses recursion• the meaning of X is that of the associated process

ProcessProcess namename

4242

SEMp

SEM := p. ‘v. SEM

‘vSEM

p

‘v

‘v. SEM

semaforo

((contcont.).)

CLOCK

‘tick ‘tick.CLOCK CLOCK‘tick

actCLOCK := ‘tick.CLOCK

CLOCK CLOCK‘tick

con

CLOCK‘ticktimer

22

4343

• the actions of P and Q are interleaved• it is possible to perform a synchronous

communication through an input action of P and an output action of Q (and vice versa)

• the operator is associative

P | Q

ParallelismParallelism

4444

((contcont.).)

par_1P P’

P | Q P’ | Q

par_2P | Q P | Q’

Q Q’

comP P’

P | Q P’ | Q’

Q Q’‘

interleaving

synchronization

Vis

23

4545

• and ‘ are corresponding actions

• processes can communicate or behaveindependently

• when communicating P and Q perform the non observable action

• communication is always synchronous and between a pair of processes

((contcont.).)

4646

The parallel operator composes processes through channelswith corresponding names

P‘a

Qa b

P‘a

Qa b

P | Q

((contcont.).)

24

4747

a.b.nil| ‘b.nil

b.nil | ‘b.nil

nil | nil

a.b.nil | nil

b.nil | nilnil | ‘b.nil

a

‘b

‘bb

‘b

a

b

LTS (a.b.nil | b’.nil)

(a.b.nil | ‘b.nil)a

‘b

b

ExampleExample

4848

P\L P’\Lres

P P’se (L ‘L )

P\L • L Vis• P can perform visible actions in L•P\L cannot perform visible actions in L• if P is a parallel process, its communication channels becomelocal

RestrictionRestriction

25

4949

(a.nil + b.nil)\{a}b

(a.nil + b.nil)b a

ExamplesExamples

((a.nil + b.nil)| ‘a.nil) ((a.nil + b.nil) | ‘a.nil)\{a}

a

b

‘a

b

5050

P[f] P’[f]rel

P P’

f

f() = bi se = ai per qualche i

altrimenti

Proprietà:

f() =

P [f] • f: Act Act by which all the actions of Act are relabeled

• it can be used to manage modularity

RelabelingRelabeling

26

5151

CCS is Turing-equivalent

• infinite state processes exist

properties are decidable if the transition systemis finite

• syntactic restrictions assure that LTS is finite•Note: LTS(p) is finite, not p

CCS CCS expressivenessexpressiveness

5252

X | b.nil| b.nil | b.nil

X

X | b.nil a.X | nil

X | nilX | b.nil| b.nila

a

a

a

a b

b

b

b. . . . .

. . . . .

X:= a.X | b.nil

No finite state automata behaves as LTS(X)

Infinite LTSInfinite LTS

27

5353

a.P P

act

P+Q P’sum1

P P’P+Q Q’

sum2 Q Q’

P|Q P’|Qpar1

P P’

P|Q P|Q’par2

Q Q’

P|Q

P’|Q’com

P P’ Q‘a

Q’

P\L P’\Lres

P P’ (L ‘L)P[f] f P’[f]

relP P’

X P’con

P P’ X:=P

SOSSOSCCSCCS

5454

Process equivalenceProcess equivalence

EquivalentEquivalent processesprocesses exhibitexhibit the the samesame ““behaviorbehavior””

28

5555

LTS LTS Equivalence (Equivalence (LTSLTS))

LTS

Processes P and Q, are LTS equivalent (P LTS Q) iffLTS(P) = LTS(Q)

a.nil | b.nil

nil|b.nil a.nil|nil

nil|nil

a.nil|b.nil

a

a

b

b

a.b.nil + b.a.nil

b.nil a.nil

nil

a

a

b

b

a.b.nil + b.a.nil

5656

LTSLTS problemsproblems

a.nila.nil | | b.nilb.nil LTSLTS a.b.nila.b.nil + + b.a.nilb.a.nil

X:= X:= a.a.Xa.a.X, Y:=, Y:=a.Ya.Y X X LTSLTS YY

ThisThis equivalenceequivalence isis tootoo low low levellevel

29

5757

String Equivalence (String Equivalence (SS))Two processes are string equivalent if they can perform the same sequences of actions

W S Z

X :=a.a.X

Y

Y := a.YX S Y

a.X

X

a a Y a

Z:= a.(b.nil + c.nil)

cb

Za

W := a.b.nil +a.c.nil

W aa

cb

5858

S S problemsproblems1. Terminating processes

2. Non determinism

3. Non observable action

c

P aa

cb

Qa

b

P:= a.b.nil+a.c.nil Q := a.(b.nil+c.nil)

P S Q

aQ nilP a P:=a..nil Q:=a.nil

P S Q

aP nila Q a

P:=a.nil +a.P

Q:=a.QP S Q

30

5959

Strong Equivalence (Strong Equivalence (~)~)

•• P e Q are P e Q are ““strong equivalentstrong equivalent”” ifif itit isis notnotpossiblepossible toto distinguishdistinguish theirtheir externalexternalbehaviorsbehaviors

•• ThisThis equivalenceequivalence solvessolves problemproblem 1 1 ((terminationtermination) & 2 (non ) & 2 (non determinismdeterminism))

6060

ExamplesExamplesP:=a.(b.nil+c.nil) Q:=a.b.nil+a.c.nil

PQ

a

cb

a

b c

aStrong

equivalent

P:=a.a.P Q:= a.Q

P Qaaa

Strongequivalent

31

6161

Results Results

P ~ Q P ~ Q impliesimplies P P SS QQ

~ = ~ = S S on on deterministicdeterministic systemssystems

6262

Specification and verification of Specification and verification of concurrent systemsconcurrent systems

The logic languagesThe logic languages

32

6363

Systems verificationSystems verification How the introduced concepts can help in verifying How the introduced concepts can help in verifying

properties of a concurrent system? properties of a concurrent system?

Consider a simple communication protocol whereConsider a simple communication protocol where thethe sendersender process receives a message from outside and transmits process receives a message from outside and transmits

it to the it to the mediummedium processprocess mediummedium either in turn transmits the message to the either in turn transmits the message to the receiverreceiver

process or loses it, in this case it asks for a retransmissionprocess or loses it, in this case it asks for a retransmission receiverreceiver transmits the message outside and transmits the message outside and acknoledgesacknoledges the the

sender for the end of transmission; after the sender for the end of transmission; after the ackack sender can sender can accept a new message.accept a new message.

6464

Communication protocolCommunication protocol

Sender := in.Sender := in.’’sm.Send1sm.Send1Send1 :=lm.Send1 :=lm.’’sm.Send1 + sm.Send1 + ack.Senderack.SenderMedium := sm.Med1Medium := sm.Med1Med1 := Med1 := ’’rm.Mediumrm.Medium + + ..’’lm.Mediumlm.MediumReceiver := Receiver := rm.rm.’’out.out.’’ack.Receiverack.Receiver

Protocol:= (Sender | Medium |Receiver)Protocol:= (Sender | Medium |Receiver)\\{{sm,lm,rm,acksm,lm,rm,ack}}

33

6565

Protocol

inin

smsmrmrm

lmlm

smsmackack

‘outout

LTSLTS11

inin

6666

System propertiesSystem properties The protocol should assure that each accepted message The protocol should assure that each accepted message

exits the process, even if not immediately. exits the process, even if not immediately.

In terms of equivalence, this could mean that In terms of equivalence, this could mean that LTS1LTS1(from the point of view of the external (from the point of view of the external behaviorbehavior) be ) be equivalent to another transition system in which only equivalent to another transition system in which only the actions in and the actions in and ‘‘out are sequentially performed out are sequentially performed forever. forever.

See See LTS2 LTS2 in the following slidein the following slide

34

6767

inin ‘outout

LTSLTS22 LTSLTS11

i.e., the two transition systems should be strong equivalentbut the protocol can loop forever losing messages and thus

LTSLTS22

6868

System verificationSystem verification What if the property required for the protocol What if the property required for the protocol

is that of having the possibility of transmitting is that of having the possibility of transmitting the received message outside?the received message outside?

Strong equivalence is not adequate: but can I Strong equivalence is not adequate: but can I define a weaker equivalence for each property?define a weaker equivalence for each property?

Choose another line of thought:Choose another line of thought:–– Give another different system specification, for Give another different system specification, for

example not operational, and compare the two.example not operational, and compare the two.

35

6969

Logic languagesLogic languages Logic languages allow the specification of sequential, Logic languages allow the specification of sequential,

concurrent, nondeterministic, reactive, realconcurrent, nondeterministic, reactive, real--time time systems. systems.

Logic languages allow a descriptive specification of Logic languages allow a descriptive specification of system system behaviorbehavior: each formula specifies a property of : each formula specifies a property of the system. the system.

7070

Logic languagesLogic languages–– Propositional logicPropositional logic Each formula expresses an absolute truth starting Each formula expresses an absolute truth starting

from known facts.from known facts.–– Il Il risultatorisultato delladella valutazionevalutazione didi unauna formula formula dipendedipende solo solo

daidai valorivalori cheche assumonoassumono i i simbolisimboli didi proposizioneproposizione. .

–– Predicate logicPredicate logic Each formula expresses a relative truth with Each formula expresses a relative truth with

respect to particular sets of the world. respect to particular sets of the world. –– EsisteEsiste un x tale un x tale cheche A(xA(x))

–– Modal logicModal logic Each formula expresses a relative truth with Each formula expresses a relative truth with

respect to a world and such truth can change from respect to a world and such truth can change from a world to another in a particular universe.a world to another in a particular universe.

36

7171

Syntax of a logic language Syntax of a logic language

The syntax of a logic language is given The syntax of a logic language is given throughthrough

–– Formulae: correct sequences of symbols Formulae: correct sequences of symbols belonging to a given alphabetbelonging to a given alphabet

–– Inference rules: rules that derive formulae Inference rules: rules that derive formulae from formulaefrom formulae

–– Axioms: formulae known trueAxioms: formulae known true

7272

SemanticsSemantics ofof a a logiclogic languagelanguage The formula semantics is a truth value The formula semantics is a truth value

determined through the interpretation.determined through the interpretation.–– In the predicate logics an interpretation is a pair In the predicate logics an interpretation is a pair

II=(D, =(D, ))

wherewhere a a associates each symbol (constant, variable, associates each symbol (constant, variable, function) with an element (or function) with an element (or nn--pleple of elements) of of elements) of D; D; each proposition or predicate is associated with a each proposition or predicate is associated with a truth value. truth value.

–– In the modal logics an interpretation is a pairIn the modal logics an interpretation is a pairI=(W, R), I=(W, R),

where where WW is called universe and is composed of a set is called universe and is composed of a set of worlds (of worlds (WW11, , …… ,,WWnn) linked together through the ) linked together through the relation relation RR. Each . Each WWii= = (D, (D, ). ).

37

7373

Examples Examples

((aab)b)((ccdd))

““x, x, pari(xpari(x))”” , where, where pari(xpari(x)=)=tttt if (x if (x modmod 2)=0, else ff2)=0, else ff

““it is possibleit is possible”” ““a a bb””–– This formula can be false independently from the This formula can be false independently from the

truth value that the interpretation of one world in truth value that the interpretation of one world in the universe associates with the universe associates with ““a a bb””..

7474

Extensional and Extensional and intensionalintensionallogicslogics

Classic logics are Classic logics are extensionalextensional: the truth value of each : the truth value of each formula derives from that of the subformula derives from that of the sub--formulae and the formulae and the meaning of the operators. meaning of the operators.

Modal logic is Modal logic is intensionalintensional: the truth value of a formula : the truth value of a formula does not necessarily derive from that of the subdoes not necessarily derive from that of the sub--formuaeformuae and the meaning of the operators. and the meaning of the operators.

The universe changes its characteristics depending The universe changes its characteristics depending on the relation type (a relation is symmetric, another on the relation type (a relation is symmetric, another one is transitive, and so on)one is transitive, and so on)

38

7575

Modal operatorsModal operators Fundamental modal operators areFundamental modal operators are

[][] its meaning is its meaning is ““necessarilynecessarily””

<><> its meaning is its meaning is ““possiblypossibly””–– The operators are dual: The operators are dual: –– given the formula given the formula <><> = = [][]

7676

Modal Logic models.Modal Logic models. A formula is true in a world A formula is true in a world WWii, if it is true in , if it is true in WWii and in all worlds and in all worlds

reachable from reachable from WWii through R. through R.

A formula is true in an universe if it is true in all worlds in A formula is true in an universe if it is true in all worlds in the the universe.universe.

An interpretation in which all modal axioms are true is called aAn interpretation in which all modal axioms are true is called amodelmodel. In the predicate calculus all interpretations are models . In the predicate calculus all interpretations are models since axioms are true in all interpretations. since axioms are true in all interpretations.

The modal axioms define the type of R: a valid formula is true iThe modal axioms define the type of R: a valid formula is true in all n all universes in which R is of a given type (thus not in all universes in which R is of a given type (thus not in all interpretations). interpretations).

39

7777

UniversoUniverso W=({WW=({W11,W,W22,W,W33,W,W44,W,W55,W,W66}, R)}, R)

WW22 (b(b)=)=tttt (a(a)=ff)=ff WW66 (b(b)=ff )=ff (a(a)=ff)=ff

[][] aabb ee’’ falsafalsa inin WW22

W1

W5

W4

W3

W2

W6

7878

Temporal logicTemporal logic•• Temporal logicTemporal logic is a particular modal logic where the worlds of an is a particular modal logic where the worlds of an

universe are temporal instants connected by a reflexive and universe are temporal instants connected by a reflexive and transitive relation R: thus R establishes a partial ordering transitive relation R: thus R establishes a partial ordering among worlds. among worlds.

•• The operators The operators [][] e e <> <> mean mean ““foreverforever”” e e ““sometimesometime””, , respectively.respectively.

•• A formula is true if it is true in all instants starting from thA formula is true if it is true in all instants starting from the e initial one (being R reflexive and transitive, all successive initial one (being R reflexive and transitive, all successive instants are reachable).instants are reachable).

•• Given a system (program), the set of computation of the system Given a system (program), the set of computation of the system is an universe. is an universe.

40

7979

System specification through System specification through temporal logictemporal logic

Temporal logic allows the definition of system Temporal logic allows the definition of system properties that hold during the time. properties that hold during the time.

The semantics of specification languages for The semantics of specification languages for communicatincommunicatin systems (CCS for example) is an LTS (systems (CCS for example) is an LTS (PP, , Act, Act, ).).

LTS can be used also to give semantics to formulae of LTS can be used also to give semantics to formulae of an action logic. an action logic.

8080

Proof methodsProof methods To prove that a formula (corresponding to a system To prove that a formula (corresponding to a system

property) is true in the given interpretation it can be property) is true in the given interpretation it can be used a theorem used a theorem proverprover: the : the proverprover is based on the is based on the axioms and the inference rules.axioms and the inference rules.

This method is complex and not automatable.This method is complex and not automatable. When the system is finite state it can be verified if a When the system is finite state it can be verified if a

structure representing the system is a structure representing the system is a model for the model for the given formula given formula by means of an algorithm traversing the by means of an algorithm traversing the structure and analyzing the related substructure and analyzing the related sub--formulae in formulae in each reached state. each reached state.

This method is called This method is called Model checking: Model checking: it is automatable. it is automatable.

41

8181

Temporal logic models.Temporal logic models. An LTS that is the semantics of a concurrent system An LTS that is the semantics of a concurrent system

must be a model for a temporal logic formula. must be a model for a temporal logic formula.

LTSsLTSs give the tree of the system computations. give the tree of the system computations.

Temporal logics that have LTS as models are called Temporal logics that have LTS as models are called branching time logic, in opposite to linear time logic. branching time logic, in opposite to linear time logic.

8282

HennessyHennessy--Milner Logic (HML)Milner Logic (HML)::= ::= tttt | ff | | ff | 1 1 22 | | 1 1 22 | [| [a]a] | | <a><a>

aaActAct[[a]a] after each occurrence of action after each occurrence of action a,a, the resulting the resulting

process process must verify property must verify property <a><a> at least an action at least an action aa is required to occur and the is required to occur and the

resulting resulting process must verify property process must verify property

For example, For example, <a><a>tttt requires the ability of performing requires the ability of performing aa; ; where where [a]ff[a]ff expresses the inability to perform such expresses the inability to perform such action. action.

42

8383

Satisfaction (1)Satisfaction (1) Given a formula Given a formula , the processes satisfying , the processes satisfying can be singled out can be singled out

through the following rules defined on the structure of the through the following rules defined on the structure of the formula. Given a process formula. Given a process pp, , pp satisfies satisfies (written p (written p ||══ ) in one ) in one the cases belowthe cases below

pp ||══ tttt , , pp ||══ ffff pp ||══ iffiff p p ||══ and and pp ||══ pp ||══ iffiff pp ||══ or or pp ||══ pp ||══ [a][a]iffiff qq {{pp’’ : : p pp p’’ }. }. qq ||══ pp ||══ <a><a>iffiff qq {{pp’’ : : p pp p’’}. }. qq ||══

Note that, from Note that, from definiondefinion of of ||══ [[a]tta]tt is equivalent to is equivalent to tttt <a>ff<a>ff is equivalent to is equivalent to ffff

α

α

8484

Satisfaction (2)Satisfaction (2) Given the transition system representing the process p, Given the transition system representing the process p,

LTS(pLTS(p)) satisfies property satisfies property iffiff is verified in its initial is verified in its initial statestate. .

The initial state of The initial state of LTS(pLTS(p) is that corresponding to p.) is that corresponding to p. LTS(pLTS(p) represents the universe and from its initial ) represents the universe and from its initial

state all other states are reachable. state all other states are reachable. If and only if two transition systems (or processes) are If and only if two transition systems (or processes) are

strong equivalent, they satisfy the same set of HML strong equivalent, they satisfy the same set of HML formulae.formulae.

HML is called HML is called adequate to strong equivalenceadequate to strong equivalence since no since no formula is able to distinguish two strong equivalent formula is able to distinguish two strong equivalent transition system (or processes).transition system (or processes).

43

8585

Examples Examples

Are the transition systems LTS(p1) and LTS(q1) Are the transition systems LTS(p1) and LTS(q1) models for the formulae models for the formulae , , and and ? ? =[a](<b>=[a](<b>tttt <c><c>tttt))= [a](<b>= [a](<b>tttt <c><c>tttt))=<a>[=<a>[b]ffb]ff

p1

p2q2 q3

q1

ab ca a

b c

8686

Examples (2)Examples (2) And are LTS( pAnd are LTS( p22) and LTS( q) and LTS( q11) models for the formulae ) models for the formulae and and ??

=[a](<b>=[a](<b>tttt <c><c>tttt))=<a>[=<a>[b]ffb]ff

p2 p2 ||══ e q1 e q1 ||══ , , mentrementre p2 p2 ||══ e q1 e q1 ||══ . .

p1 q3

q2

b ca

a

a

b c

p2

q1

44

8787

Extensions to HMLExtensions to HML [[K]K] <K><K> KK Act (if Act is infinite, K can be Act (if Act is infinite, K can be

infinite too)infinite too)[[K]K] = ([a= ([a11] ] .. .. [a[ann]) ]) , , aaii KK<K><K> = (= (<a<a11> > .. .. <a<ann>) >) , , aaii KK

[[--K] K] <<--K> K> [[--K]K] = ([a= ([a11] ] .. .. [a[ann]) ]) , , aaii ActAct--KK<<-- K>K> = (= (<a<a11> > .. .. <a<ann>) >) , , aaii ActAct--KK

[[--] ] <<--> > [[--]] = ([a= ([a11] ] .. .. [a[ann]) ]) , , aaii ActAct-- <<-- >> = (= (<a<a11> > .. .. <a<ann>) >) , , aaii ActAct--

α

α

8888

Some hints on the expressivity of Some hints on the expressivity of HMLHML

[[--]ff]ff Termination Termination

<<-->>tttt Vitality Vitality

<<-->>tttt [[--a]ffa]ff Obligation Obligation

The properties above are properties that have no time The properties above are properties that have no time duration.duration.

Consider the property Consider the property ““action a can always be action a can always be performedperformed””:: Does the formula <a>Does the formula <a>tttt express this property?express this property?

45

8989

Some hints on the expressivity of Some hints on the expressivity of HML (cont.)HML (cont.)

<a><a>tttt is true on both the transition systems belowis true on both the transition systems below

But the second transition system is able to perform a But the second transition system is able to perform a only in the initial state.only in the initial state.

I need some form of recursion in the application of the I need some form of recursion in the application of the formula to simulate the flowing of the time. formula to simulate the flowing of the time.

aa

9090

Modal Modal --calculuscalculus::= ::= tttt ff ff 1 1 22 1 1 22 [K][K] <K><K>

ZZ. . ZZ. . ZZKKActAct

ZZ. . and and ZZ. . are fixed point formulae (greatest and are fixed point formulae (greatest and least respectively), where the operators least respectively), where the operators ZZ e e ZZ bind bind the occurrences ofthe occurrences of the variablethe variable Z in Z in Closed formulae Closed formulae do not contain free variables. The constants do not contain free variables. The constants tttt andand ffffcan be obtained also as can be obtained also as Z.ZZ.Z and and Z.ZZ.Z, respectively. , respectively.

--calcoluscalcolus too is too is adeguateadeguate to strong equivalence.to strong equivalence.

46

9191

Satisfaction Satisfaction

pp ||══ ZZ iffiff pp VV(Z)(Z)–– Closed formulae are independent from Closed formulae are independent from

evaluation evaluation pp ||══ Z.Z. iffiff pp ||══ ZZkk.. for each for each kk pp ||══ ZZ .. iffiff pp ||══ ZZkk.. for some for some kk

To define satisfaction of recursive operators we can To define satisfaction of recursive operators we can apply a technique of syntactic approximation that builds apply a technique of syntactic approximation that builds a finite chain of non recursive formulae until that one a finite chain of non recursive formulae until that one representing the fixed point of the equation Z= representing the fixed point of the equation Z= is is obtained. obtained.

9292

Approximants Approximants

ZZ00.. = = tttt ZZk+1k+1.. = = [([(ZZkk../Z]/Z]

ZZ00.. = ff= ff ZZk+1k+1.. = = [([(ZZkk../Z]/Z]

[[/Z] substitutes each free occurrence of Z /Z] substitutes each free occurrence of Z in in with with ..

47

9393

operatoroperator Z.Z. means that infinite sequences of actions leading means that infinite sequences of actions leading

to the satisfaction of to the satisfaction of are required. are required. the chain of formulae that approximate the meaning the chain of formulae that approximate the meaning

of of ZZ.<a>Z is .<a>Z is ZZ00.<a>Z=.<a>Z=ttttZZ11.<a>Z=<a>.<a>Z=<a>ttttZZ22.<a>Z=<a><a>.<a>Z=<a><a>tttt

……....Thus the formula is satisfied by a transition Thus the formula is satisfied by a transition system that contains at least an infinite path, system that contains at least an infinite path, starting from the initial state, which contains only starting from the initial state, which contains only a infinite number of consecutive a.a infinite number of consecutive a.In other words: In other words: ““action a can always be performedaction a can always be performed””::

9494

operatoroperator Z.Z. means that finite sequences of actions leading to means that finite sequences of actions leading to

the satisfaction of the satisfaction of are required. are required. the chain of formulae that approximate the meaning of the chain of formulae that approximate the meaning of

Z.[a]ZZ.[a]Z is is ZZ00.[a]Z=ff.[a]Z=ffZZ11.[a]Z=[.[a]Z=[a]ffa]ffZZ22.[a]Z=[.[a]Z=[a][a]ffa][a]ff

……....

Thus the formula is satisfied by a transition system Thus the formula is satisfied by a transition system that contains paths, starting from the initial state, that contains paths, starting from the initial state, which contain only a finite number of consecutive a.which contain only a finite number of consecutive a.

48

9595

Some hints on the expressivity Some hints on the expressivity (cont.)(cont.)

The property The property ZZ.<a>Z is true on the first .<a>Z is true on the first trasitiontrasitionsystem and false on the second one. system and false on the second one.

Now time duration can be expressed. Now time duration can be expressed.

a

a

9696

Examples Examples 11== ZZ.(<.(<-->>tttt [[--]Z) ]Z)

DeadlockDeadlock--freenessfreeness 22== ZZ.([.([--]ff ]ff <<-->Z)>Z)

CanCan--deadlockdeadlock 33== ZZ.(<.(<-->>tttt [[--a]Z)a]Z)

““after a finite amount of time after a finite amount of time aa will be executedwill be executed”” 44== Z.([a]ffZ.([a]ff [[--]Z)]Z)

““henceforth henceforth aa will not be executed will not be executed ““

49

9797

Communication protocolCommunication protocol

Protocol:= (Sender | Medium |Receiver)Protocol:= (Sender | Medium |Receiver)\\ {{sm,lm,rm,acksm,lm,rm,ack}}

Sender := in.Sender := in.’’sm.Send1sm.Send1Send1 :=lm.Send1 :=lm.’’sm.Send1 + sm.Send1 + ack.Senderack.SenderMedium :=sm.Med1Medium :=sm.Med1Med1 :=Med1 :=‘‘rm.Mediumrm.Medium + + t.t.’’lm.Mediumlm.MediumReceiver :=Receiver :=rm.rm.’’out.out.’’ack.Receiverack.Receiver

9898

protocol

in

smrm

lm

smack

‘out

in

50

9999

Properties of the protocolProperties of the protocol= = [in] ([in] (YY. <. <‘‘out>out>tttt <<--’’out>Y)out>Y)

Each message that Sender receives Each message that Sender receives maymay be output by be output by Receiver. Receiver.

= = [in] ([in] (YY. <. <-->>tttt [[--’’out]Y)out]Y) Each message that Sender receives, sooner or later, Each message that Sender receives, sooner or later, isis

output by Receiver.output by Receiver.

is true on is true on protocolprotocol , while , while is false. is false.

100100

Model Checking complexityModel Checking complexity When recursive operators occur in a formula, their When recursive operators occur in a formula, their

fixpointsfixpoints can be computed separately only if the can be computed separately only if the formulae are alternationformulae are alternation--free and in this case free and in this case verification algorithms have linear complexity.verification algorithms have linear complexity.–– [in] ([in] (YY. <out>. <out>tttt <<--out>Y)out>Y)–– This formula is alternationThis formula is alternation--freefree

For formulae with level of alternation bigger than 1, For formulae with level of alternation bigger than 1, verification algorithms have a complexity exponential in verification algorithms have a complexity exponential in the alternation level.the alternation level.

51

101101

Model Checking complexityModel Checking complexity

The complexity of model checking a The complexity of model checking a property with dimension m (number of property with dimension m (number of logic operators) on a transition system logic operators) on a transition system with dimension n (number of states) is of with dimension n (number of states) is of order (n x m) in the best case.order (n x m) in the best case.

102102

Model checking environmentsModel checking environments

They minimize with respect to different equivalence They minimize with respect to different equivalence relations.relations.

They build the LTS for a specification program, CCS They build the LTS for a specification program, CCS programs or LOTOS programs for example programs or LOTOS programs for example

They include the implementation of model checking They include the implementation of model checking algorithms for different logics (algorithms for different logics (-- calcoluscalcolus, CTL etc)., CTL etc).

52

103103

Problems Problems The number of states of the transition systems is The number of states of the transition systems is

limited.limited.

Constraints are imposed on the structure of the Constraints are imposed on the structure of the formulae to maintain a low complexity of the model formulae to maintain a low complexity of the model checking algorithmschecking algorithms

Parallel composition of processes produces an Parallel composition of processes produces an exponential growth of the number of states of the exponential growth of the number of states of the resulting transition systemresulting transition system