| 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 | 도서상태 대출가능 | 반납예정일 | 예약 | 서비스 |
컨텐츠정보
목차
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
정보제공 :
