Specification and Development of Interactive Systems

by Broy, Manfred; Stolen, Ketil

• ISBN13: 9780387950730
• ISBN10: 0387950737
• Format: Hardcover
• Copyright: 2001-01-01
• Publisher: Springer-Verlag New York Inc

Summary

Today's distributed systems are characterized by interactions-often complex-between many different hardware and software components cooperating and exchanging information. To simplify development of interactive systems and facilitate communication and documentation, experts of varying disciplines employ descriptions, or specifications, of a given system's behavior and/or structure.Specification and Development of Interactive Systems offers a unique approach to program and software development suitable for large distributed systems, with an emphasis on modular system development and systems engineering. The authors build a basic method, called FOCUS, that enables interactive systems to be described by characterizing their histories of message interaction. The method covers functional requirements, timing, structure, and implementation issues of systems. In addition, the book describes how to connect the models and techniques to tables and diagram-based methods popular in practical systems engineering.Topics and features: * Specification of interface behavior and modular top-down system development * Specification of time and the modeling of hardware/software systems * Interface refinement and the modeling of development steps leading from one level of abstraction to the next * State transition diagrams and tables and the usage of common description techniques, such as found in UMLThis 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. The reader gains a comprehensive understanding of all fundamental models, techniques, and methods for interactive system design. The book is an essential resource for all researchers and professionals in computer science, software systems engineering and computer engineering.

Table of Contents

Preface	v
Examples	xiii
Introduction	1	(18)
Systems	2	(1)
Specifications	3	(3)
Refinement	6	(1)
Application Domains	7	(1)
Development Process and Methodology	8	(1)
Rationale of Focus	9	(4)
Classification of Modeling Techniques	9	(1)
Description Paradigm	10	(3)
Overview of the Book	13	(2)
Part 1: Introductory Section	13	(1)
Part 2: Mathematical Foundations	14	(1)
Part 3: Specification	14	(1)
Part 4: Refinement	14	(1)
How the Book Should Be Read	15	(4)
A Guided Tour	19	(32)
Plan for the Tour	19	(2)
Station 1: Unbounded Buffer	21	(8)
Streams	21	(1)
Informal Specification	22	(1)
Task 1.1: A/G Specification	23	(2)
Task 1.2: Equational Specification	25	(3)
Task 1.3: Equational Specification with Local States	28	(1)
Station 2: Unbounded Lossy Buffer	29	(4)
Task 2.1: Combined Equational and A/G Specification with Oracles	30	(2)
Task 2.2: Table-Based Specification	32	(1)
Station 3: Driver	33	(1)
Station 4: Composite Specifications	34	(3)
Task 4.1: Graphical Specification	34	(1)
Task 4.2: Constraint-Based Specification	34	(1)
Task 4.3: Behavioral Refinement	35	(1)
Task 4.4: Glass-Box Specification	36	(1)
Station 5: Time-Sensitive Buffer	37	(3)
Timed Streams	37	(1)
Task 5.1: A/G Specification	38	(1)
Timed versus Untimed Specifications	39	(1)
Task 5.2: Conditional Behavioral Refinement	40	(1)
Station 6: Timed Lossy Buffer	40	(5)
Informal Specification	41	(1)
Task 6.1: A/G Specification	41	(1)
Task 6.2: Conditional Interface Refinement	42	(3)
Station 7: Timed Driver	45	(3)
Task 7.1: A/G Specification	46	(1)
Task 7.2: State Transition Diagram	47	(1)
Task 7.3: Refinement	48	(1)
Station 8: Timed Composite Specification	48	(3)
Development	48	(3)
Basics	51	(6)
Sets	51	(1)
Tuples	52	(1)
Functions	53	(1)
Types	53	(1)
Logic	54	(3)
Streams	57	(12)
Formal Definition of Streams	59	(1)
Basic Operators on Streams	59	(3)
Additional Operators on Streams	62	(2)
Formal Definition of Timed Streams	64	(1)
Operators on Timed Streams	65	(4)
Specifications	69	(32)
Classification of Specifications	70	(3)
Elementary Specifications	73	(11)
Syntax	73	(1)
Examples	74	(6)
Semantics	80	(3)
Graphical Representation of Syntactic Interfaces	83	(1)
Composite Specifications	84	(4)
Graphical Style	84	(1)
Constraint Style	85	(1)
Operator Style	86	(1)
Methodological Advice	87	(1)
Black-Box and Glass-Box Views	88	(1)
Parameterized Specifications	89	(2)
Sheafs and Replications	91	(10)
Sheafs of Channels	91	(2)
Specification Replication	93	(3)
Dependent Replications	96	(5)
Examples	101	(14)
Alternating Bit Protocol	101	(3)
Steam Boiler	104	(3)
Memory Components	107	(8)
Basic Definitions	108	(1)
Sequential Memory Component	109	(1)
Concurrent Memory Component	110	(1)
Repetitive Memory Component	111	(4)
Properties of Specifications	115	(22)
Safety and Liveness Properties	115	(6)
Formalization of Safety	116	(2)
Formalization of Liveness	118	(1)
Decomposition into Safety and Liveness Parts	119	(1)
Safety and Liveness for Specifications	120	(1)
Realizability	121	(8)
Strategies	123	(1)
Weak and Strong Realizability	123	(3)
Full Realizability	126	(2)
Preserving Realizability by Composition	128	(1)
Causality for Specifications	129	(8)
Adding Causality to Specifications	129	(2)
A Proof Principle Based on Strong Causality	131	(1)
Causality and Feedback	132	(5)
Equational Specification of State Transitions	137	(24)
I/O Transitions	140	(7)
Local States	147	(3)
Control States	150	(5)
Oracles	155	(6)
Access Control System	161	(16)
System Architecture	161	(4)
Functional Properties of the Controllers	165	(5)
Central Controller	165	(1)
Local Controller	165	(3)
Panel Controller	168	(2)
Introducing Exception Handling	170	(2)
Imposing Timing Constraints	172	(5)
Introducing Timeouts	172	(3)
Imposing Constraints on the Response Time	175	(2)
Tables and Diagrams	177	(18)
State Transition Tables	178	(4)
State Transition Diagrams	182	(6)
Semantics of State Transition Tables and Diagrams	188	(7)
Syntax of State Transition Diagrams	188	(1)
Semantics of Deterministic State Transition Diagrams	189	(2)
Semantics of Nondeterministic State Transition Tables	191	(4)
Abracadabra Protocol	195	(18)
Informal Specification	195	(3)
Protocol Data Units and Parameters	196	(1)
Connection Phase	197	(1)
Data Transfer Phase	197	(1)
Disconnection Phase	197	(1)
Error Phase	198	(1)
Underlying Medium Service	198	(1)
Formalization	198	(15)
Overall Structure	198	(2)
Sender/Receiver	200	(2)
Formalization of State Transitions	202	(11)
A/G Specifications	213	(16)
Simple Examples	214	(7)
Semantics	221	(2)
More Examples	223	(6)
Memory with Locking	229	(12)
Black-Box Description	229	(5)
Distributed Implementation	234	(7)
Refinement	241	(12)
Behavioral Refinement	242	(1)
Interface Refinement	242	(3)
Conditional Refinement	245	(2)
Verification	247	(2)
Glass-Box Refinement	249	(1)
Development Method	250	(3)
Behavioral Refinement	253	(16)
Definition	253	(1)
Simple Examples	254	(5)
Logical Properties	259	(1)
More Examples	260	(2)
Synchronizing the Communication	262	(7)
Interface Refinement	269	(30)
Definition	270	(1)
A Priming Convention for Channel Identifiers	271	(1)
Simple Examples	272	(9)
Methodological Issues	281	(3)
Refinement Pairs	281	(1)
Schematic Interface Refinement	282	(1)
Realizability	283	(1)
Logical Properties	284	(2)
More Examples	286	(6)
Generalizing Interface Refinement	292	(7)
Conditional Refinement	299	(16)
Definition	299	(2)
Simple Examples	301	(2)
Logical Properties	303	(1)
More Examples	304	(11)
Final Remarks	315	(4)
How Our Approach Generalizes	315	(1)
What We Did Not Cover	316	(3)
A. Operators for Stream Tuples	319	(4)
Generalized Operators	319	(1)
Tuple Filtering Operator	320	(1)
Timed Filtering Operator	321	(2)
B. Glossary of Terms	323	(6)
Sets	323	(1)
Tuples	323	(1)
Functions	324	(1)
Types	324	(1)
Logic	325	(1)
Arithmetics	325	(1)
Streams	326	(1)
Tuples of Streams	327	(1)
Specifications	327	(1)
Strategies	328	(1)
Refinement	328	(1)
Frame Labels	328	(1)
C. Bibliography	329	(6)
D. Glossary	335	(10)
Index	345