HOME > 상세정보


Principles of the Spin model checker

Principles of the Spin model checker (4회 대출)

Ben-Ari, M. , 1948-.
서명 / 저자사항
Principles of the Spin model checker / Mordechai Ben-Ari.
London :   Springer ,   c2008.  
xv, 216 p. : ill. ; 24 cm.
9781846287695 (pbk.) 1846287693 (pbk.) 1846287707 (ebook) 9781846287701 (ebook)
Includes bibliographical references (p. [209]-210) and index.
Computer software -- Verification.
000 01028camuu22003137a 4500
001 000045434650
005 20080417153347
008 071114s2008 enka b 001 0 eng
010 ▼a 2007941384
015 ▼a GBA771506 ▼2 bnb
020 ▼a 9781846287695 (pbk.)
020 ▼a 1846287693 (pbk.)
020 ▼a 1846287707 (ebook)
020 ▼a 9781846287701 (ebook)
035 ▼a (KERIS)REF000014887835
040 ▼a UKM ▼c UKM ▼d BAKER ▼d BTCTA ▼d YDXCP ▼d C#P ▼d DLC ▼d 211009
042 ▼a lccopycat
050 0 0 ▼a QA76.76.V47 ▼b B46 2008
082 0 4 ▼a 005.14 ▼2 22
090 ▼a 005.14 ▼b B456p
100 1 ▼a Ben-Ari, M. , ▼d 1948-.
245 1 0 ▼a Principles of the Spin model checker / ▼c Mordechai Ben-Ari.
260 ▼a London : ▼b Springer , ▼c c2008.
300 ▼a xv, 216 p. : ▼b ill. ; ▼c 24 cm.
504 ▼a Includes bibliographical references (p. [209]-210) and index.
630 0 0 ▼a SPIN (Computer file)
650 0 ▼a Computer software ▼x Verification.
945 ▼a KINS


No. 소장처 청구기호 등록번호 도서상태 반납예정일 예약 서비스
No. 1 소장처 과학도서관/Sci-Info(2층서고)/ 청구기호 005.14 B456p 등록번호 121168423 도서상태 대출가능 반납예정일 예약 서비스 B M



Foreword.- Preface.- Sequential Programming in PROMELA.- A First Program in PROMELA.- Random Simulation- Data Types.- Operators and Expressions.- Control Statements.- Repetitive Statements.- Jump Statements.- Verification of Sequential Programs.- Assertions.- Verifying a program in Spin.- Concurrency.- Interleaving.- Atomicity.- Interactive Simulation.- Interference between processes.- Sets of Processes.- Interference revisited.- Deterministic Sequences of Statements.- Verification with Assertions.- The critical section problem.- Synchroniztion.- Synchronization by blocking.- Executability of statements.- State transition diagrams.- Atomic sequences of statements.- Semaphores.- Nondeterminism in models of concurrent systems.- Termination of Processes.- Verification with Temporal Logic.- Beyond Assertions.- Introduction to linear temporal logic.- Safety properties.- Liveness properties.- Fairness.- Duality.- Verifying correctness without ghost variables.- Modeling a non-critical section.- Advanced temporal specifications.- Data and Program Structures.- Arrays.- Type Definitions.- The preprocessor.- Inline.- Channels.- Channels in PROMELA.- Rendezvous channels.- Buffered channels.- Checking the content of a channel.- Random receive .- Sorted send .- Copying the value of a message .- Polling .- Comparing rendezvous and buffered channels.- Nondeterminism .- Nondeterministic finite automata.- VN: Visualizing Nondeterminism.- NP problems.- Advanced Topics in PROMELA .- Specifiers for Variables.- Predefined variables.- Priority.- Modeling Exceptions.- Reading from standard input.- Embedded C code.- Advanced Topics in SPIN .- How SPIN searches the state space.- Optimizing the performances of verifications.- Never claims.- Non-progress cycles.- Case Studies .- Channels as data structures.- Nondeterministic algorithms.- Modeling a real-time scheduling algorithm.- Fischer's algorithm.- Modeling distributed systems.- The Chandy-Lamport algorithm for global snapshots.- TheChandy-Lamport snapshot algorithm in PROMELA.- Verification of the snapshot algorithm.- Appendix A: Software Tools.- Appendix B: Links.- References.- Index

정보제공 : Aladin

관련분야 신착자료

Burns, Brendan (2023)
김성기 (2023)