Introduction to the Formal Design of Real-Time Systems

by David F. Gray

• ISBN13: 9783540761402
• ISBN10: 3540761403
• Format: Nonspecific Binding
• Copyright: 2012-12-06
• Publisher: Springer Nature

Summary

Based on the premise that in order to design things correctly, it is necessary to thoroughly understand the design as it evolves from problem definition through to solution validation. DLC: Real-time data processing.

Table of Contents

Preface	vii
Intended Audience	viii	(1)
Layout	viii	(1)
Acknowledgements	ix
1 Scene Set	1	(46)
1.1 Making Models	3	(6)
1.2 Lies, Damn Lies and Models	9	(4)
1.3 Abstraction, Atomicity and Algebras	13	(7)
1.3.1 Algebras, Specifications and Other Related Things	16	(4)
1.4 Labelled Transition Systems	20	(7)
1.4.1 An Algebra of Transition Systems	20	(7)
1.5 One at Once, All Together and In Time	27	(14)
1.5.1 A Process Algebra for Sequential Systems	28	(6)
1.5.2 A Process Algebra for Concurrent Systems	34	(7)
1.6 Real-Time Systems	41	(6)
2 Concurrency and Communication	47	(66)
2.1 Concurrency -- Defining the Problems	49	(9)
2.2 Programming Domain Solutions	58	(52)
2.2.1 Mutual Exclusion	58	(1)
2.2.2 Critical Sections	59	(21)
2.2.3 Synchronisation	80	(8)
2.2.4 Semaphores	88	(7)
2.2.5 Monitors	95	(15)
2.3 Review and Rethink	110	(3)
3 Message Passing	113	(26)
3.1 Choosing the Best	114	(5)
3.1.1 The Contenders	115	(3)
3.1.2 The Choosing	118	(1)
3.2 Blocking Send	119	(10)
3.3 CCS (Calculus of Communicating Systems)	129	(6)
3.4 Rendezvous	135	(3)
3.5 Conclusion	138	(1)
4 Synchronous Calculus of Communicating Systems	139	(162)
4.1 An Overview of SCCS	144	(21)
4.2 Plain SCCS	165	(34)
4.2.1 Naming of Parts	165	(7)
4.2.2 Basic Operators and Propositions	172	(27)
4.3 Recursion	199	(10)
4.3.1 Recursion in SCCS Terms	199	(4)
4.3.2 Derived Agents	203	(6)
4.4 Actions, Particles, Composites and All Sorts	209	(3)
4.5 Synchronisation	212	(17)
4.5.1 Interaction	212	(17)
4.6 Constructional Design	229	(13)
4.6.1 Scoping and Synchronisation	229	(4)
4.6.2 Choice of Choices	233	(3)
4.6.3 Example -- Software Interrupts	236	(2)
4.6.4 Distributing Pruning over Product	238	(4)
4.7 Message Passing	242	(12)
4.7.1 Parameter Passing	242	(5)
4.7.2 Message Passing	247	(4)
4.7.3 Predicated Choice	251	(3)
4.8 Agents Lurking	254	(38)
4.8.1 Delay Delta	254	(7)
4.8.2 One Agent Waits	261	(7)
4.8.3 Both Agents Wait	268	(7)
4.8.4 Examples	275	(8)
4.8.5 Message Passing and Waiting	283	(9)
4.9 Specifications and Proof	292	(9)
4.9.1 Mutual Exclusion	293	(4)
4.9.2 Livelock -- Software Scheduler	297	(1)
4.9.3 Deadlock -- Software Scheduler	298	(2)
4.9.4 Comments	300	(1)
5 Equivalence	301	(32)
5.0 The Need For Equivalence	301	(3)
5.1 Traces	304	(2)
5.2 From Traces to Bisimulations	306	(1)
5.3 Bisimulation	307	(26)
5.3.1 Strong Bisimulation	309	(2)
5.3.2 From Strong Bisimulation to an Equivalence	311	(8)
5.3.3 Observational Equivalence	319	(9)
5.3.4 Observational Congruence	328	(5)
6 Automating SCCS	333	(46)
6.0 Concurrency Work Bench: an Introduction	333	(4)
6.1 CWB and Agent Behaviours	337	(18)
6.2 Agents, Bisimulation and CWB	355	(23)
6.3 Comments	378	(1)
7 Proving Things Correct	379	(54)
7.1 Modal Logics	380	(38)
7.1.1 Hennessy-Milner Logic	380	(14)
7.1.2 Propositional Modal Mu-Calculus -- Modal Logic Plus Fixed Points	394	(24)
7.2 Modal Logic, CWB and Satisfaction	418	(15)
8 End End Note	433	(2)
Appendix 1 Some of the More Useful SCCS Propositions	435	(6)
Appendix 2 Notation Used Throughout the Book	441	(10)
References	451	(4)
Index	455