HOME > 상세정보

상세정보

Abstract state machines : a method for high-level system design and analysis

Abstract state machines : a method for high-level system design and analysis

자료유형
단행본
개인저자
Borger, E. (Egon) , 1946-. Stark, Robert F 1963-
서명 / 저자사항
Abstract state machines : a method for high-level system design and analysis / Egon Borger, Robert Stark.
발행사항
Berlin ;   New York :   Springer ,   2003.  
형태사항
x, 438 p. : ill. ; 24 cm. + 1 CD-ROM (4 3/4 in.).
ISBN
3540007024 (alk. paper)
서지주기
Includes bibliographical references (p. [379]-428) and index.
일반주제명
System design. Computer software -- Development. Embedded computer systems.
000 01133camuu22003014a 4500
001 000045310056
005 20061128132514
008 030407s2003 gw a b 001 0 eng
010 ▼a 2003050371
020 ▼a 3540007024 (alk. paper)
035 ▼a (KERIS)REF000007219391
040 ▼a DLC ▼c DLC ▼d DLC ▼d 211009
042 ▼a pcc
050 0 0 ▼a QA76.9.S88 ▼b B66 2003
082 0 0 ▼a 004.2/1 ▼2 21
090 ▼a 004.21 ▼b B732a
100 1 ▼a Borger, E. ▼q (Egon) , ▼d 1946-.
245 1 0 ▼a Abstract state machines : ▼b a method for high-level system design and analysis / ▼c Egon Borger, Robert Stark.
260 ▼a Berlin ; ▼a New York : ▼b Springer , ▼c 2003.
300 ▼a x, 438 p. : ▼b ill. ; ▼c 24 cm. + ▼e 1 CD-ROM (4 3/4 in.).
504 ▼a Includes bibliographical references (p. [379]-428) and index.
538 ▼a System requirements: Internet browser, AcrobatReader, PowerPoint, 15 MB free hard disk space.
650 0 ▼a System design.
650 0 ▼a Computer software ▼x Development.
650 0 ▼a Embedded computer systems.
700 1 ▼a Stark, Robert F ▼d 1963-
945 ▼a KINS

소장정보

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

컨텐츠정보

저자소개

Egon Borger(지은이)

Robert F. Stark(지은이)

정보제공 : Aladin

목차

'1 Introduction.- 1.1 Goals of the Book and Contours of its Method.- 1.1.1 Stepwise Refinable Abstract Operational Modeling.- 1.1.2 Abstract Virtual Machine Notation.- 1.1.3 Practical Benefits.- 1.1.4 Harness Pseudo-Code by Abstraction and Refinement.- 1.1.5 Adding Abstraction and Rigor to UML Models.- 1.2 Synopsis of the Book.- 2 ASM Design and Analysis Method.- 2.1 Principles of Hierarchical System Design.- 2.1.1 Ground Model Construction (Requirements Capture).- 2.1.2 Stepwise Refinement (Incremental Design).- 2.1.3 Integration into Software Practice.- 2.2 Working Definition.- 2.2.1 Basic ASMs.- 2.2.2 Definition.- 2.2.3 Classification of Locations and Updates.- 2.2.4 ASM Modules.- 2.2.5 Illustration by Small Examples.- 2.2.6 Control State ASMs.- 2.2.7 Exercises.- 2.3 Explanation by Example: Correct Lift Control.- 2.3.1 Exercises.- 2.4 Detailed Definition (Math. Foundation).- 2.4.1 Abstract States and Update Sets.- 2.4.2 Mathematical Logic.- 2.4.3 Transition Rules and Runs of ASMs.- 2.4.4 The Reserve of ASMs.- 2.4.5 Exercises.- 2.5 Notational Conventions.- 3 Basic ASMs.- 3.1 Requirements Capture by Ground Models.- 3.1.1 Fundamental Questions to be Asked.- 3.1.2 Illustration by Small Use Case Models.- 3.1.3 Exercises.- 3.2 Incremental Design by Refinements.- 3.2.1 Refinement Scheme and its Specializations.- 3.2.2 Two Refinement Verification Case Studies.- 3.2.3 Decomposing Refinement Verifications.- 3.2.4 Exercises.- 3.3 Microprocessor Design Case Study.- 3.3.1 Ground Model DLXseq.- 3.3.2 Parallel Model DLXpar Resolving Structural Hazards.- 3.3.3 Verifying Resolution of Structural Hazards (DLXpar).- 3.3.4 Resolving Data Hazards (Refinement DLXdata).- 3.3.5 Exercises.- 4 Structured ASMs (Composition Techniques).- 4.1 Turbo ASMs (seq, iterate, submachines, recursion).- 4.1.1 Seq and Iterate (Structured Programming).- 4.1.2 Submachines and Recursion (Encapsulation and Hiding).- 4.1.3 Analysis of Turbo ASM Steps.- 4.1.4 Exercises.- 4.2 Abstract State Processes (Interleaving).- 5 Synchronous Multi-Agent ASMs.- 5.1 Robot Controller Case Study.- 5.1.1 Production Cell Ground Model.- 5.1.2 Refinement of the Production Cell Component ASMs.- 5.1.3 Exercises.- 5.2 Real-Time Controller (Railroad Crossing Case Study).- 5.2.1 Real-TimeProcess Control Systems.- 5.2.2 Railroad Crossing Case Study.- 5.2.3 Exercises.- 6 Asynchronous Multi-Agent ASMs.- 6.1 Async ASMs: Definition and Network Examples.- 6.1.1 Mutual Exclusion.- 6.1.2 Master-Slave Agreement.- 6.1.3 Network Consensus.- 6.1.4 Load Balance.- 6.1.5 Leader Election and Shortest Path.- 6.1.6 Broadcast Acknowledgment (Echo).- 6.1.7 Phase Synchronization.- 6.1.8 Routing Layer Protocol for Mobile Ad Hoc Networks.- 6.1.9 Exercises.- 6.2 Embedded System Case Study.- 6.2.1 Light Control Ground Model.- 6.2.2 Signature (Agents and Their State).- 6.2.3 User Interaction (Manual Control).- 6.2.4 Automatic Control.- 6.2.5 Failure and Service.- 6.2.6 Component Structure.- 6.2.7 Exercises.- 6.3 Time-Constrained Async ASMs.- 6.3.1 Kermit Case Study (Alternating Bit/Sliding Window).- 6.3.2 Processor-Group-Membership Protocol Case Study.- 6.3.3 Exercises.- 6.4 Async ASMs with Durative Actions.- 6.4.1 Protocol Verification using Atomic Actions.- 6.4.2 Refining Atomic to Durative Actions.- 6.4.3 Exercises.- 6.5 Event-Driven ASMs.- 6.5.1 UML Diagrams for Dynamics.- 6.5.2 Exercises.- 7 Universal Design and Computation Model.- 7.1 Integrating Computation and Specification Models.- 7.1.1 Classical Computation Models.- 7.1.2 System Design Models.- 7.1.3 Exercises.- 7.2 Sequential ASM Thesis (A Proof from Postulates).- 7.2.1 Gurevich's Postulates for Sequential Algorithms.- 7.2.2 Bounded-Choice Non-Determinism.- 7.2.3 Critical Terms for ASMs.- 7.2.4 Exercises.- 8 Tool Support for ASMs.- 8.1 Verification of ASMs.- 8.1.1 Logic for ASMs.- 8.1.2 Formalizing the Consistency of ASMs.- 8.1.3 Basic Axioms and Proof Rules o


정보제공 : Aladin

관련분야 신착자료

김자미 (2021)