04/11/23 1

Metodi formali dello sviluppo software

a.a.2013/2014

Prof. Anna Labella

04/11/23 2

Esempio di verifica: mutua esclusione

04/11/23 3

Esempio di verifica: mutua esclusione

Altri requisiti:

Un processo può sempre richiedere di entrare nella sezione critica

L’alternanza non è necessaria

04/11/23 4

Espressività di LTL

Sicurezza G ( c1 c2)

Liveness G (ti Fci)

Non blocco ????Non stretta sequenzializzazione: neghiamo

G ( c1 ( c1W ( c1( c1W c2) ))

04/11/23 5

Esempio di verifica: mutua esclusione

Ogni singolo processon t c n t c ……..

Un processo può sempre richiedere di entrare nella sezione critica

L’alternanza non è necessaria

04/11/23 6

Primo tentativo

04/11/23 7

Espressività di LTLSicurezza G ( c1 c2) vero

Liveness G (ti Fci) falso

s0s1s3s7s1s3s7….

Non blocco ????Non stretta sequenzializzazione: neghiamo

G ( c1 ( c1W ( c1( c1W c2) )) falso

s0s5s3s4s5s3s4….

04/11/23 8

Secondo tentativo

04/11/23 9

Maggiore espressività

Poter quantificare sui cammini

In LTL la soddisfacibilità era definita soltanto sui cammini; da qui veniva passata allo stato iniziale

04/11/23 10

Semantics of X and U

Semantics of X: |= X p

• Semantics of U: |= p U q

1 |= p

j |= p

i |= q

04/11/23 11

Linear time and Branching time

Linear: only one possible future in a moment– Look at individual computations

Branching: may split to different courses depending on possible futures– Look at the tree of computations

s0

s0

s1

s3

s0 s2

s0

s0 s1

...

s0 s2 s3s1 ...

s0 s0 s1s0 ...

s0 s0 s1s1 ......

s0

s2

s3

s1

04/11/23 12

Computation Trees

State transition structure(Kripke Model)

Infinite computation tree for initial state s1

a

b

a ac

ac

ac

ac

s1

s3

s1

s2

a

b ac

04/11/23 13

CTL – Computation Tree Logic

Path quantifiers - describe branching structure of the tree– A (for all computation paths)

– E (for some computation path = there exists a path)

Temporal operators - describe properties of a path through the tree– X (next time, next state)

– F (eventually, finally)

– G (always, globally)

– U (until)

– W (weak until)

04/11/23 14

Operators and Quantifiers State operators

– G a : a holds globally– F a : a holds eventually– X a : a holds at the next state– a U b: a holds until b holds– A W b: a holds until b possibly holds

– Path quantifiers– E: along at least one path (there exists …)– A: along all paths (for all …)

04/11/23 15

CTL – Computational Tree Logic CTL* - a powerful branching-time temporal

logic CTL – a branching-time fragment of CTL* In CTL every temporal operator (G,F,X,U,W)

must be immediately preceded by a path quantifier (A,E)

We need both state formulae and path formulae to recursively define the logic

04/11/23 16

CTL Formulas

Temporal logic formulas are evaluated w.r.to a state in the model

State formulas– apply to a specific state

Path formulas– apply to all states along a specific path

04/11/23 17

Basic CTL Formulas E X (f)

– true in state s if f is true in some successor of s (there exists a next state of s for which f holds)

A X (f)– true in state s if f is true for all successors of s (for all next

states of s f is true)

E G (f)– true in s if f holds in every state along some path

emanating from s (there exists a path ….)

A G (f)– true in s if f holds in every state along all paths emanating

from s (for all paths ….globally )

04/11/23 18

Basic CTL Formulas - cont ’d E F (g)

– there exists a path which eventually contains a state in which g is true

A F (g)– for all paths, eventually there is state in which g holds

E F, A F are special case of E [f U g], A [f U g]– E F (g) = E [ true U g ], A F (g) = A [ true U g ]

f U g (f until g)– true if there is a state in the path where g holds, and

at every previous state f holds

04/11/23 19

CTL Operators - examples

so |= E F g

g

so so

g

g

g

so |= A F g

so |= E G g

gso

g

g

so |= A G g

so

g

g

g

g

gg

04/11/23 20

CTL

Temporal operators are immediately preceded by a path quantifier

The following are a complete set ¬p, p q , AX p , EX p , A( p U q),

E( p U q) Others can be derived

– EF p E(true U P)– AF p A(true U p)– EG p ¬ AF ¬ p– AG p ¬ EF ¬p

04/11/23 21

Typical CTL Formulas

E F ( start ¬ ready )– eventually a state is reached where start holds and ready

does not hold

A G ( req A F ack )– any time request occurs, it will be eventually acknowledged

A G ( E F restart )– from any state it is possible to get to the restart state

04/11/23 22

Minimal set of CTL Formulas Full set of operators

– Boolean: ¬, , , , – temporal: E, A, X, F, G, U, W

Minimal set sufficient to express any CTL formula– Boolean: ¬, – temporal: E, X, U

Examples: f g = ¬(¬f ¬g), F f = true U f , A (f ) = ¬E(¬f )

04/11/23 23

Logica CTL (CTL*)

04/11/23 24

LTL: le formule sono pensate precedute da A Linear time operators. The following are a complete set

¬ p , p q , X p, p U q

Others can be derived– p q ¬(¬p ¬q) – p q ¬p q– F p (true U p)– G p (p U false)

04/11/23 25

LTL and CTL

LTL (Linear Temporal Logic) - Reasoning about infinite sequence of states π: s0, s1, s2, …

CTL (Computation Tree Logic) – Reasoning on a computation tree. – Temporal operators are immediately preceded by a path

quantifier (e.g. A F p ) CTL vs. LTL – different expressive power

– EFp is not expressible in LTL– FGp is not expressible in CTL

04/11/23 26

CTL* Syntax

An atomic proposition is a state formula A state formula is also a path formula If a, b are state formulae, so are ¬a, ab, ab, If p is a path formula, E p is a state formula If p, q are path formulae, so are ¬p, pq, pq If p, q are path formulae, so are X p, pUq, pRq,

04/11/23 27

CTL* Semantics If formula q holds at state s (path ), we write: s

|= q ( |= q) s |= p, p A iff p L(s) [label of s] s |= ¬ a, iff s |# a s |= a b, iff s |= a and s |= b s |= E p, iff from state s, s.t. |= p

|= ¬ p, iff |# p |= p q, iff |= p and |= q |= X p, iff 1 |= p (p reachable in next state)

04/11/23 28

Logiche a confronto

04/11/23 29

Logiche a confronto

04/11/23 30