Bérard, Béatrice , Bidoit, Michel , Finkel, Alain , Laroussinie, Francois , Petit, Antoine , Petrucci, Laure , Schnoebelen, Philippe , Pierre McKenzie

Systems and Software Verification

Name: Systems and Software Verification
Price: 6400.00 HUF
Availability: BackOrder
Author: Bérard, Béatrice
ISBN: 3540415238

Model-Checking Techniques and Tools

Bérard, Béatrice, Bidoit, Michel, Finkel, Alain, Laroussinie, Francois, Petit, Antoine, Petrucci, Laure, Schnoebelen, Philippe, Pierre McKenzie - Systems and Software Verification, Berlin-Heidelberg-New York 2001 antikvár könyv

(0 vélemény)

Antikvár könyv

Jelenleg nem elérhető. Tájékoztató ár az utolsó ismert ár és az aktuálisan érvényes kedvezmény alapján: 7 200 Ft. Jegyezze elő, és elsőként értesítjük, ha újra rendelhető!

Bővebb leírás

ISBN:	3540415238
Kiadó:	Springer-Verlag
Kiadás éve:	2001
Kiadás helye:	Berlin-Heidelberg-New York
Kötés típusa:	kemény papír
Terjedelem:	190 oldal
Nyelv:	angol
Méret:	Szélesség: 16.00 cm, Magasság: 24.00 cm
Súly:	0.00 kg
Kategória:	Természettudomány / Matematika / Idegennyelv / Nyelvek / Angol / Műszaki / Számítástechnika, Informatika

Ajánlja ismerőseinek is!

Kívánságlistára teszem ezt a könyvet!

Megnézem a tartalomjegyzéket!

Part I. Principles and Techniques

  Introduction                            3 

1.Automata                                5
  1.1Introductory Exarnples               5
  1.2A Few Definitions                    9
  1.3A Printer Manager                    11
  1.4A Few More Variables 
  1.5Synchronized Product                 14
  1.6Synchronization by kIessage Passing  21
  1.7Synchronization by Shared Variables  24

2.Temporal Logic                          27
  2.1The Language of Temporal Logic_      28
  2.2The Formai Syntax of Temporal Logic  32
  2.3The Semantics of Temporal Logic      33
  2.4PLTL and CTL: Two Temporal Logics    35
  2.5The Expressivity of CTL*             37

3.Model Checking                          39
  3.11VIodel Checking CTL                 39
  3.2Model Checking PLTL                  42
  3.3The State Explosion Problem          45

4.Symbolic Model Checking                 47
  4.1Symbolic Computation of State Sets   47
  4.2Binary Decisibn Diagrams (BDD)       51
  4.3Representing Automata by BDDs        54
  4.4BDD-based Model Checking             56

5.Timed Automata                          59
  5.1Description of 'a Timed Automaton    60
  5.2Networks of Timed Automata
     and Synchronization                  69


X	
',111(111.,
5.3	
Varianis and Extensioil,; ol	
Hi
5.4	
Timed 'Pemporal Logic	
5.5	
Timed Model Cheeking	
Conclusion 	
(■'; 
(1ti
73
Part II. Specifying with Temporal Logic
Introduction	
77
6.	
Reachability Properties	
79
6.1	
Reachability in Temporal Logic 	
79
6.2	
Model Checkers and Reachability	
80
6.3	
Computation of the Reachability Graph	
80
7.	
Safety Properties 	
83
Safety Properties ir Temporal Logic 	
83
7.2	
A Formai Definition 	
84
7.3	
Safety Properties in Practice	
86
7.4	
The History Variables. Method 	
87
8.	
Liveness Properties	
91
8.1	
Simple Liveness in Temporal Logic 	
92
8.2	
Arc Liveness Properties Useful? 	
92
8.3	
Liveness in the Model, Liveness in the Properties 	
94
8.4	
Verification undor Liveness Hypotheses	
96
8.5	
Bounded Liveness 	
97
9.	
Deadlock-freeness	
99
9.1	
Safety? Liveness?	
99
9.2	
Deadlock-freeness for a Given Automaton 	
99
9.3	
Beware of Abstractions! 	
101
10. Fairness Properties 	
103
10.1 Fairness in Temporal Logic 	
103
10.2 Fairness and Nondeterminism 	
104
10.3 Fairness Properties and Fairness Hypotheses 	
104
10.4 Strorig Fairness and Weák Fairness 	
106
10.5 Fairnoss in the Model or in the Property? 	
107
11. Abstraction Methods 	
109
11.1 When Is Model Abstraction Required? 	
110
11.2 Abstraction l:)y State Merging	
110
11.3 What Can Be Proved in the Abstract A utomaton? 	
110
11.4 Abstraction on the Variables 	
114
C11,11(1111	
XI
11	
11,:•11:14.1	
■111	
1■N	
•
•	
,,,,,	
111.;
11,1i	
()1):.,11 v(1.	
A	
.	
,	
,	
.....	
•	
I '.).1)
( ;onelusion	
12!)
I'1■1•1, III. Sonu, Tools
I iil,rodu('t,ion 	
 12!)
I2, ti M V	
8 yG11)■	
1\10(1(11 	
11
12,1 wha(,	
wii	
v.,
I.I
	
'1 I
Kynclti,,Giiiiig A 111.(Hwtl.a	
I 'IG
I )0,11H,Gt,111()11 and	
SI,11(11('s 	
1;:\IV 1111)11,w,r,)pliv 	
'18
Ii
HI'IN'ti
13,3 I	
w((!ti 	
1:{,	
IIII
ion
1h)(11111(111;iii■HI anc1 CaS(`
IM)1.1(wl';11)IiV	
II
	
1 1,I 1,1( :N/CPN - Col(tort(.1 Petri Nets 	
I\\ 11;11 ( an Wc I)c xviI Ii 1)HsIGN/CPN'?  	
1.
I I	
I )1!<;N/t
I	
wil 
II	
I
I	
I! 
1.11 I )■w111114111:It ion IIII(1 Case	
111
I)IIIN,/('I',	
1111)11(w,r;ipliy 	
I I '1)A A I, 	
I")	
I	
\\	
1)()	
■';
I	
\ \	
1'.	
1,■Is	
l';
11111,11 -v-icii-; wii,11	
111)1)AA1,  	
:■
:1	
I	
1111111.11i)p.	
;1
1'•■	
\
11, i■	
1 h
I JI'I' \ \I.
12.2 KN,I \Ps  
12.1 1)<'scribilw,
I 3, SPIN (:()Iiiimmicating Automata 
I:1.1 \\11L (':111 Wc 1)o Wil-,11 SPIN?


XII  Contents

16. KRONOS — Model Checking of Real-time Systems 161
    16.1 What Can We Do with KRONOS?             161
    16.2 KRONOS' Essentials                      161
    16.3 Describing Automata                      162
    16.4 Synchronized Product                    164
    16.5 Mode] Checking                          165
    16.6 Documentation and Case Studies          167
    KRONOS Bibliography                          167
17. HYTECH — Linear Hybrid Systems               169
    17.1 What Can We Do With HYTECH?             169
    17.2 HYTECH'S Essentials                     169
    17.3 Describing Automata                     170
    17.4 System Analysis                         172
    17.5 Parametric Analysis                     174
    17.6 Documentation and Case Studies          176
    HYTECH Bibliography                          176
Main Bibliography                                179
Index                                            183

Systems and Software Verification

Model-Checking Techniques and Tools

Antikvár könyv

Bővebb leírás

Vélemények a könyvről

Központi raktár és ügyfélszolgálat

1045 Bp. Istvántelki út 10-12.
Telefon: +36 1 443-3460
Hétfőtől - péntekig 8 óra 30 perctől 17 óráig.

Belvárosi kereskedés

1053 Bp, Múzeum körút 39.
Telefon: +36 1 443-3461
Hétfőtől - péntekig 10 órától 18 óráig
szombaton zárva.

Központi raktár és ügyfélszolgálat

Belvárosi kereskedés

Központi raktár és ügyfélszolgálat

Belvárosi kereskedés

1045 Bp. Istvántelki út 10-12.
Telefon: +36 1 443-3460
Hétfőtől - péntekig 8 óra 30 perctől 17 óráig.

1053 Bp, Múzeum körút 39.
Telefon: +36 1 443-3461
Hétfőtől - péntekig 10 órától 18 óráig és szombaton zárva.

Nem támogatott böngészőt használ.

Kérjük használjon modern böngészőt például: Microsoft Edge, Safari, Google Chrome, Firefox...

Megértésüket köszönjük,

Régikönyvek.hu

/

/

/

Systems and Software Verification

Systems and Software Verification

Model-Checking Techniques and Tools

Antikvár könyv

Bővebb leírás

Vélemények a könyvről

Hírlevél feliratkozás

Központi raktár és ügyfélszolgálat

1045 Bp. Istvántelki út 10-12.Telefon: +36 1 443-3460Hétfőtől - péntekig 8 óra 30 perctől 17 óráig.

Belvárosi kereskedés

1053 Bp, Múzeum körút 39.Telefon: +36 1 443-3461Hétfőtől - péntekig 10 órától 18 óráig szombaton zárva.

Központi raktár és ügyfélszolgálat

Belvárosi kereskedés

Központi raktár és ügyfélszolgálat

Belvárosi kereskedés

1045 Bp. Istvántelki út 10-12.Telefon: +36 1 443-3460Hétfőtől - péntekig 8 óra 30 perctől 17 óráig.

1053 Bp, Múzeum körút 39.Telefon: +36 1 443-3461Hétfőtől - péntekig 10 órától 18 óráig és szombaton zárva.

Nem támogatott böngészőt használ.

Kérjük használjon modern böngészőt például: Microsoft Edge, Safari, Google Chrome, Firefox...

Megértésüket köszönjük,

Régikönyvek.hu

1045 Bp. Istvántelki út 10-12.
Telefon: +36 1 443-3460
Hétfőtől - péntekig 8 óra 30 perctől 17 óráig.

1053 Bp, Múzeum körút 39.
Telefon: +36 1 443-3461
Hétfőtől - péntekig 10 órától 18 óráig
szombaton zárva.

1045 Bp. Istvántelki út 10-12.
Telefon: +36 1 443-3460
Hétfőtől - péntekig 8 óra 30 perctől 17 óráig.

1053 Bp, Múzeum körút 39.
Telefon: +36 1 443-3461
Hétfőtől - péntekig 10 órától 18 óráig és szombaton zárva.