Del i serien Monographs in Computer Science

Specification and Development of Interactive Systems

Focus on Streams, Interfaces, and Refinement

Inbunden, Engelska, 2001

AvManfred Broy,Ketil Stølen

719 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt för medlemmar vid köp för minst 249 kr.

Finns i fler format (1)

Häftad

719 kr

Skickas inom 10-15 vardagar

Today's distributed systems are characterized by interactions, often complex, between many different hardware/software components cooperating and exchanging information. To reduce the complexity of the development of interactive systems, experts employ descriptions, or specifications, of a given system's behavior and/or structure. This book provides a mathematical and logical foundation for the specification and development of interactive systems based on a model that describes systems in terms of their input/output behavior. Based on the model, the authors build a basic method, called FOCUS, that enables interactive systems to be described by characterizing their histories of message interaction. The book progresses from an introduction and guided tour of FOCUS through streams, specifications and their properties, and behavioral, interface, and conditional refinements.

Produktinformation

Utgivningsdatum2001-04-27
Mått155 x 235 x 24 mm
Vikt660 g
FormatInbunden
SpråkEngelska
SerieMonographs in Computer Science
Antal sidor348
Upplaga2001
FörlagSpringer-Verlag New York Inc.
ISBN9780387950730

Tillhör följande kategorier

Systemvetenskap och AI inom Data och IT
Programvaruutveckling inom Data och IT

1. Introduction.- 1.1 Systems.- 1.2 Specifications.- 1.3 Refinement.- 1.4 Application Domains.- 1.5 Development Process and Methodology.- 1.6 Rationale of Focus.- 1.7 Overview of the Book.- 1.8 How the Book Should Be Read.- 2. A Guided Tour.- 2.1 Plan for the Tour.- 2.2 Station 1: Unbounded Buffer.- 2.3 Station 2: Unbounded Lossy Buffer.- 2.4 Station 3: Driver.- 2.5 Station 4: Composite Specifications.- 2.6 Station 5: Time-Sensitive Buffer.- 2.7 Station 6: Timed Lossy Buffer.- 2.8 Station 7: Timed Driver.- 2.9 Station 8: Timed Composite Specification.- 3. Basics.- 3.1 Sets.- 3.2 Tuples.- 3.3 Functions.- 3.4 Types.- 3.5 Logic.- 4. Streams.- 4.1 Formal Definition of Streams.- 4.2 Basic Operators on Streams.- 4.3 Additional Operators on Streams.- 4.4 Formal Definition of Timed Streams.- 4.5 Operators on Timed Streams.- 5. Specifications.- 5.1 Classification of Specifications.- 5.2 Elementary Specifications.- 5.3 Composite Specifications.- 5.4 Black-Box and Glass-Box Views.- 5.5 Parameterized Specifications.- 5.6 Sheafs and Replications.- 6. Examples.- 6.1 Alternating Bit Protocol.- 6.2 Steam Boiler.- 6.3 Memory Components.- 7. Properties of Specifications.- 7.1 Safety and Liveness Properties.- 7.2 Realizability.- 7.3 Causality for Specifications.- 8. Equational Specification of State Transitions.- 8.1 I/O Transitions.- 8.2 Local States.- 8.3 Control States.- 8.4 Oracles.- 9. Access Control System.- 9.1 System Architecture.- 9.2 Functional Properties of the Controllers.- 9.3 Introducing Exception Handling.- 9.4 Imposing Timing Constraints.- 10. Tables and Diagrams.- 10.1 State Transition Tables.- 10.2 State Transition Diagrams.- 10.3 Semantics of State Transition Tables and Diagrams.- 11. Abracadabra Protocol.- 11.1 Informal Specification.- 11.2 Formalization.- 12. A/G Specifications.- 12.1 Simple Examples.- 12.2 Semantics.- 12.3 More Examples.- 13. Memory with Locking.- 13.1 Black-Box Description.- 13.2 Distributed Implementation.- 14. Refinement.- 14.1 Behavioral Refinement.- 14.2 Interface Refinement.- 14.3 Conditional Refinement.- 14.4 Verification.- 14.5 Glass-Box Refinement.- 14.6 Development Method.- 15. Behavioral Refinement.- 15.1 Definition.- 15.2 Simple Examples.- 15.3 Logical Properties.- 15.4 More Examples.- 15.5 Synchronizing the Communication.- 16. Interface Refinement.- 16.1 Definition.- 16.2 A Priming Convention for Channel Identifiers.- 16.3 Simple Examples.- 16.4 Methodological Issues.- 16.5 Logical Properties.- 16.6 More Examples.- 16.7 Generalizing Interface Refinement.- 17. Conditional Refinement.- 17.1 Definition.- 17.2 Simple Examples.- 17.3 Logical Properties.- 17.4 More Examples.- 18. Final Remarks.- 18.1 How Our Approach Generalizes.- 18.2 What We Did Not Cover.- A. Operators for Stream Tuples.- A.l Generalized Operators.- A.2 Tuple Filtering Operator.- A.3 Timed Filtering Operator.- B. Glossary of Terms.- B.l Sets.- B.2 Tuples.- B.3 Functions.- B.4 Types.- B.5 Logic.- B.6 Arithmetics.- B.7 Streams.- B.8 Tuples of Streams.- B.9 Specifications.- B.10 Strategies.