Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://lvk.cs.msu.su/~dimawolf/SoftwareReliability/Lection03.pdf Äàòà èçìåíåíèÿ: Tue Sep 23 01:52:22 2014 Äàòà èíäåêñèðîâàíèÿ: Sat Apr 9 22:59:09 2016 Êîäèðîâêà: Ïîèñêîâûå ñëîâà: landing

(LTS). LTS
. .. , , ..

3:



· · · · · · · , (LTS) , ,
2


· · , , · , ·
3




...
, ,

4


, :
() ()

( )



( )

()



()




5


, :
() () ()

( )



( )

()



()




6



int main (){ printf( }

t tl tll l tl l t



(ACFG)

l l l

l=T t=T



, ,

( TAKEOFF (!FALL) U (LANDED))

llt ttl ll ll

t l

t



( )

7


(LTS)

8


LTS
0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
: (, x, y)
9


LTS
0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
: (, x, y)
10

S

L



· AP , · · , · ­ «»
11


LTS
0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
: (, x, y)
12

S

L


LTS
0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
: (, x, y)
13

S

L


LTS
0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
: (, x, y)
14


?
«» ,

15


int p; Process Prod(){ while(1) 1.1: if(p < 2) 1.2: p += 1; } process Cons() {

Prod

LTS Cons

while(1) 2.1: if(p > 0) 2.2: p -= 1; } : ( Prod, Cons, p)
( . , )
, 16



· , · = · LTS

17



· - · , , , · ,

18



· Prod Cond · , · ­ ­ 19


­ !
· :
­ ()
·
Prod Cons

ELF System board

Processor

20


­ !
· :
­
·

21


­ !
· :
­
· ,

22


LTS
· LTS , AP {a}
a a a a


23

­


LTS
· LTS ,

? ?

24

­



s
a

s a

25




26



· TS , : · TS :

· ,

s0 I
27



· , . · TS .

28




29




30




31




32




33



· s S ( ) TS, ,

· Reach(TS) , TS.

34



· ; . (). · .

35


· :



· ( ): · :

«»
36





a p 0 2

a p 0 b p 1

a a !a

!a !b !a !b

a
b ab

!a
a

!a !b
!a !b
37

a



· :
a - « » b - « »

· :
« »

· :
aüüüüübü... üüüüüüü...

· :
aüüüüüüü... aüüüübaü...
38



· · :

(2 AP )





· TS :

TS

Traces(TS )
TS(P)

P


39



() ()

( )



( )

()



()




40



· I:

I (tr) , ,


N ­ , ­ N , : N AP {T, } ,

n 0, p AP

(n, p) T p L(s)
41



· tr tr' , :

· , tr' () tr ( tr tr'),

: N N : n, k N n k (n) (k)
n N , p AP' (n, p) ' ((n), p) 42

AP' AP



p=T q=F r=F p=T q=F r=T p=F q=F r=F p=F q=T r=T p =F q =T r=F

AP={p,q,r}

p=T q=F

p=T q=F

p=F q=F

p=F q=T

p=F q=T

AP'={p,q}
p=T q=F p=F q=F p=F q=T

AP'={p,q}
43



() ()

( )



( )

()



()




44



· P ­ , ­ . () P , :

,
· , :

45



· P ­ , ­ . () P , :

M P





· , :

tr Traces(TS(P))tr'Traces(TS(M )) : t r t r'
,
46





· TS , ?
­ , ­ , ­ , ­ , . . , ­ . . 47



· TS , ?

s S, L'( (s)) L(s) AP'



48



p = T,q = T a p = F,q = F q=F q=T a q=F q=T a

b
p = T,q = T T q=

b
d c q=T d q=F q= q=F e

b
e f c

d
p = F,q = T T p = T,q = F p = F,q = T e f

c

q=T
f

q=T

(P)

(M1)

(M2)

49



() ()

( )



( )

()



()




50


· , :
1. , , 2. ,



51



· , :

1.

AP APM
( )

2.

M

P
( )

· ,

52



p = T,q = T a p = F,q = F q=F q=T a q=F q=T a

b
p = T,q = T T q=

b
d c q=T d q=F q= q=F e

b
e f c

d
p = F,q = T T p = T,q = F p = F,q = T e f

c

q=T
f

q=T

(P)

(M1)

(M2)

53


­
· , p=T & q=T ­ , · , q= F q= T ­ , · q= F 3 q= T ­ 1 , 2 ­ .
54



() ()

( )



( )

()



()




55


!

56