Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://lvk.cs.msu.su/~dimawolf/SoftwareReliability/Lection05.pdf Äàòà èçìåíåíèÿ: Thu Sep 25 01:44:49 2014 Äàòà èíäåêñèðîâàíèÿ: Sat Apr 9 22:59:40 2016 Êîäèðîâêà:

(LTL)

5:

. .. , , ..
1



· · (LTL) · ,

· LTL


· ,



· ;

· ,
· , · ;

· :
· , ­ , · , ­ , · , .


­ Leslie ( Lamport)

·« »; · :
­ ( y);


·« »; · : «»
­ , ;

· ­ , ( «», )

· ­ , «»


...
· ­ («, , »). · , ? · «, !, » ­ , ; · «, , » ­ , , .


...
· « » ­ , ; · .









: "-" , -, ,




- ( , A&B B&A): " " " " " " " " " " " "



: ­ ( - ) , m , m c , , -

() ! , ,
7





TL - , ,
, , .



TL


: ; : , ; : , (. . () " «, 1987);



: (, , , ...), ,


TL

8



· p ; · p ; · p ; · p ¬q; · p , q.


?
· =>
· : « » ? ? · :
· : « » « » · « , » ?

· :
· , · , , ( ) · , , ( )

· , LTL.


LTL
· , ; · , «», «», « », . · ­ LTL. , ­ . · LTL (Amir Pnueli) 70.


· , · LTL =

LTL

+
· LTL f ::=
· p, q, ... , true false, · ( f ) ­ , · f ­ , · f1 f2 ­ .


· :

LTL

· ([]) ( ), · (<>) ,

­ () , ­ ¬ (!) ;

· :
· · · · ­

U (U) , (&&) , (pq)(qp) (||) , (->) , (<->) .

(¬pq)


·


p

s0 , s1, s2 , s3,...
· p, q:

i,i 0, p, si
· LTL:



f
[] f f Xf



s0

f
j j

si si si
s0



si si+1

j, j i : s j, j i : s si 1 f

f f


unl
: si

eWf



si

f ( si

e si

1

(eWf ))

: si
(Spin)

eUf



j, j i : s

j

f

e

k , i k j : sk

si
e e e e

sj
f






e W false true U f eWf

[]e

f
[]e eUf


p s0

p

p

p

p

p

p p p
q

p

p

si

si+
1

sn
1

sn

q

| []p | []q

| p

| [] p

| q

| [] q

| pUq | [](pUq) | [](pWq)

| qUp | [](qUp)
| qWp | []qWp


p s0

p

p

p

p

p

p p p
q

p

p

si

si+
1

sn
1

sn

q

| []p | []q

| p

| [] p

| q

| [] q

| pUq | [](pUq) | [](pWq)

| qUp | [](qUp)
| qWp | []qWp



· , p, p ­ ; · , p, p ­ .


LTL

p
p p, q p, q, r p p



() ()

[]p

> p
p <> q

p qUr
[]<> p >[]p

> p <> q

p, q






[]p

· p ;

<>[]!p

· p ; · p ; · p ¬q;
[](p->!q)

[]<>!p

· p , q.
[](p-> <>q)


LTL
LTL: >b1 !b2Ub2 []!a
!b1


3

1.

b1 , pq , !pq; .
b1 ,

2.

b

1

. 3. b1 , ­ b2, a3 ; . b1 , ­ b2, ­ a3; .

b1 !b2 b
1

!b2 b2 !a3 b2
!b2 !a3





4.

a3



LTL
LTL:
1. b1 b2 ; .

>b1 >b2
!b1


2.

b1, b2 ; . b1 , b2 ; .

b2
!b2 !b

b1


1

3.

b !b1

1

!b2




LTL
LTL: []
1. b1 b2 ; .

>b1 >b2
!b1 b2 !b1 !b2 !b1 !b2 b1



2.

b1, b2 ; . b2 ; .

b1

b2 !b1 !b2 !b1


3.

b1 !b2

b2 !b1
!b1

!b2 b1
!b2



LTL
"p q"
· p > q
· , .. ; · !pq , ; · ; · .


LTL
"p q"
· [] p > q
­ ­ ­ ­ ! [] p; ([]p) > q; ; .


LTL
"p q"
· [] (p > q)
­ , p q ; ­, ! pq ; ­ ; ­ , p q.


LTL
"p q"
· [] (p > <>q)
­ ; ­ , , q , p ­ ; ­ ; ­ , q p.


LTL
"p q"
· [] (p > X(<>q))
­ , ; ­ , p ; ­, ; ­ , p q.


LTL
"p q"
· [] (p > X(<>q)) && (<>p)
­ , ; ­ p>q;

­LTL ; ­ ?


neXt
· X :
· ; · ; · , , ; · .


,
· ­ P,
­ , , n1 n 2 n ­ 1 2 3 .
3

... ,

· E() , n1, n2, n3 (.. )
­ E() .


mutex x x = 1 (y==0) mutex++ printf
x==0 y==0 mutex==0

=0

x==1 y==0 mutex==0

x==1 x==1 x==1 x==1 x==0 y==0 y==0 y==0 y==0 y==0 mutex==0 mutex==1 mutex==1 mutex==0 mutex==0



p !q

!p q

!p q

p q

p q

!p q

p !q

1E()

p !q

!p q

p q

!p q

p !q


,
· , , E(), :



f

v E( ), v

f

· , , ; · : LTL X . · , LTL X , .


LTL


LTL

· LTL · · ( !) · «» .


LTL
· LTL () · · , ­ Unl


LTL
· LTL · ,

· , ·
«»

.


http://patterns. projects.cis.ksu.edu
(LTL/CTL/GIL)

(occurence)

(order, sequence)

(absense)

(universality)
(precedence) chain precedence (response)

(existence) bounded existence


· ­ :
r q r q r q "absense" LTL
[](!p)

http://patterns. projects.cis.ksu.edu

?
<>r -> (!p U r)

[](q -> [](!p))
[]((r && !q && <>q) -> (!p U q)) []((r && !q) -> ((!p U q) || []!p))


·

http://patterns. ­ : projects.cis.ksu.edu
"absense" LTL
r r

r
q q

q
r r q r q r

r q r q

r

r

q

r


· (p) , . · []X(p)

, LTL

true

p

· p && [](p -> X!p) && [](!p -> Xp) ­ ( p p