Introduction to the Formal Design of Real-Time Systems

Author:   David F. Gray
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Edition:   Softcover reprint of the original 1st ed. 1999
ISBN:  

9783540761402


Pages:   461
Publication Date:   01 November 1998
Format:   Paperback
Availability:   Out of stock   Availability explained
The supplier is temporarily out of stock of this item. It will be ordered for you on backorder and shipped when it becomes available.

Our Price $189.95 Quantity:  
Add to Cart

Share |

Introduction to the Formal Design of Real-Time Systems


Add your own review!

Overview

The design of concurrent and real-time systems is difficult. It is even more difficult to design them correctly. Introduction to the Formal Design of Real Time Systems is 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 and, though the simplest way to maintain such an understanding is from within a formal mathematical framework, this will only be effective if the framework is simple to understand and easy to use. This book is based on courses given to undergraduate and masters students in Electrical Engineering, Information Technology and Computer Science, and backed by copious worked examples.

Full Product Details

Author:   David F. Gray
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Edition:   Softcover reprint of the original 1st ed. 1999
Dimensions:   Width: 15.50cm , Height: 2.40cm , Length: 23.50cm
Weight:   0.720kg
ISBN:  

9783540761402


ISBN 10:   3540761403
Pages:   461
Publication Date:   01 November 1998
Audience:   College/higher education ,  Professional and scholarly ,  Postgraduate, Research & Scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   Out of stock   Availability explained
The supplier is temporarily out of stock of this item. It will be ordered for you on backorder and shipped when it becomes available.

Table of Contents

1 Scene Set.- 1.1 Making Models.- 1.2 Lies, Damn Lies and Models.- 1.3 Abstraction, Atomicity and Algebras.- 1.3.1 Algebras, Specifications and Other Related Things.- 1.4 Labelled Transition Systems.- 1.4.1 An Algebra of Transition Systems.- 1.5 One at Once, All Together and In Time.- 1.5.1 A Process Algebra for Sequential Systems.- 1.5.2 A Process Algebra for Concurrent Systems.- 1.6 Real-Time Systems.- 2 Concurrency and Communication.- 2.1 Concurrency - Defining the Problems.- 2.2 Programming Domain Solutions.- 2.2.1 Mutual Exclusion.- 2.2.2 Critical Sections.- 2.2.3 Synchronisation.- 2.2.4 Semaphores.- 2.2.5 Monitors.- 2.3 Review and Rethink.- 3 Message Passing.- 3.1 Choosing the Best.- 3.1.1 The Contenders.- 3.1.2 The Choosing.- 3.2 Blocking Send.- 3.3 CCS (Calculus of Communicating Systems).- 3.4 Rendezvous.- 3.5 Conclusion.- 4 Synchronous Calculus of Communicating Systems.- 4.1 An Overview of SCCS.- 4.2 Plain SCCS.- 4.2.1 Naming of Parts.- 4.2.2 Basic Operators and Propositions.- 4.3 Recursion.- 4.3.1 Recursion in SCCS Terms.- 4.3.2 Derived Agents.- 4.4 Actions, Particles, Composites and All Sorts.- 4.5 Synchronisation.- 4.5.1 Interaction.- 4.6 Constructional Design.- 4.6.1 Scoping and Synchronisation.- 4.6.2 Choice of Choices.- 4.6.3 Example - Software Interrupts.- 4.6.4 Distributing Pruning over Product.- 4.7 Message Passing.- 4.7.1 Parameter Passing.- 4.7.2 Message Passing.- 4.7.3 Predicated Choice.- 4.8 Agents Lurking.- 4.8.1 Delay ?.- 4.8.2 One Agent Waits.- 4.8.3 Both Agents Wait.- 4.8.4 Examples.- 4.8.5 Message Passing and Waiting.- 4.9 Specifications and Proof.- 4.9.1 Mutual Exclusion.- 4.9.2 Livelock - Software Scheduler.- 4.9.3 Deadlock - Software Scheduler.- 4.9.4 Comments.- 5 Equivalence.- 5.0 The Need For Equivalence.- 5.1 Traces.- 5.2 From Traces to Bisimulations.- 5.3 Bisimulation.- 5.3.1 Strong Bisimulation.- 5.3.2 From Strong Bisimulation to an Equivalence.- 5.3.3 Observational Equivalence.- 5.3.4 Observational Congruence.- 6 Automating SCCS.- 6.0 Concurrency Work Bench: an Introduction.- 6.1 CWB and Agent Behaviours.- 6.2 Agents, Bisimulation and CWB.- 6.3 Comments.- 7 Proving Things Correct.- 7.1 Modal Logics.- 7.1.1 Hennessy-Milner Logic.- 7.1.2 Propositional Modal Mu-Calculus - Modal Logic plus Fixed Points.- 7.2 Modal Logic, CWB and Satisfaction.- 8 End End Note.- Appendix 1 Some of the More Useful SCCS Propositions.- Appendix 2 Notation Used Throughout the Book.- References.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions
Latest Reading Guide

MRG2025CC

 

Shopping Cart
Your cart is empty
Shopping cart
Mailing List