List of Figures

Chapter 1: Introduction

Figure 1.1: Cruise control system.

Figure 1.2: Simulation of the cruise control system.

Figure 1.3: Speed input process.

Figure 1.4: Animation of the cruise control system.

Chapter 2: Processes and Threads

Figure 2.1: Light switch state machine.

Figure 2.2: ONESHOT state machine.

Figure 2.3: LTSA Animator window for SWITCH.

Figure 2.4: TRAFFICLIGHT.

Figure 2.5: DRINKS state machine.

Figure 2.6: LTSA Animator window for DRINKS.

Figure 2.7: FAULTY.

Figure 2.8: COIN.

Figure 2.9: LTSA Animator window for COIN.

Figure 2.10: BUFF.

Figure 2.11: SUM.

Figure 2.12: COUNT.

Figure 2.13: COUNTDOWN.

Figure 2.14: Operating system threads.

Figure 2.15: Implementing run() using inheritance.

Figure 2.16: Implementing run() using the Runnable interface.

Figure 2.17: THREAD life cycle.

Figure 2.18: Countdown timer class diagram.

Chapter 3: Concurrent Execution

Figure 3.1: Process switching.

Figure 3.2: Composition CONVERSE_ITCH.

Figure 3.3: Composition CLOCK_RADIO.

Figure 3.4: Composition BILL_BEN.

Figure 3.5: Composition MAKER_USER.

Figure 3.6: Composition MAKER_USERv2.

Figure 3.7: Composition FACTORY.

Figure 3.8: Process labeling in TWO_SWITCH.

Figure 3.9: Process labeling in RESOURCE_SHARE.

Figure 3.10: Relabeling in CLIENT_SERVER.

Figure 3.11: Hiding applied to USER.

Figure 3.12: Minimized LTS for USER.

Figure 3.13: Structure diagram conventions.

Figure 3.14: Two-slot buffer TWOBUF.

Figure 3.15: Resource-sharing PRINTER_SHARE.

Figure 3.16: ThreadDemo display.

Figure 3.17: ROTATOR.

Figure 3.18: ThreadDemo model.

Figure 3.19: LTSA Animator window for THREAD_DEMO.

Figure 3.20: ThreadDemo class diagram.

Chapter 4: Shared Objects and Mutual Exclusion

Figure 4.1: Ornamental Garden.

Figure 4.2: Ornamental Garden class diagram.

Figure 4.3: Garden display.

Figure 4.4: Ornamental Garden model.

Figure 4.5: LTS for TURNSTILE.

Figure 4.6: An Animator trace for the Ornamental Garden.

Figure 4.7: Corrected Garden display.

Figure 4.8: Minimized LTS for COUNTER.

Figure 4.9: Minimized LTS for DISPLAY_COUNTER.

Chapter 5: Monitors and Condition Synchronization

Figure 5.1: Car park display.

Figure 5.2: Car park model.

Figure 5.3: Car park LTS.

Figure 5.4: Car park class diagram.

Figure 5.5: Monitor wait() and notify().

Figure 5.6: Semaphore LTS.

Figure 5.7: Semaphore mutual exclusion model.

Figure 5.8: SEMADEMO LTS.

Figure 5.9: SEMADEMO display.

Figure 5.10: Bounded buffer display.

Figure 5.11: Bounded buffer model.

Figure 5.12: Bounded buffer LTS.

Chapter 6: Deadlock

Figure 6.1: MOVE process.

Figure 6.2: Printer–scanner system.

Figure 6.3: LTS for process P.

Figure 6.4: LTS for the shared printer process.

Figure 6.5: The Dining Philosophers table.

Figure 6.6: Dining Philosophers composite model.

Figure 6.7: Dining Philosophers class diagram.

Figure 6.8: Dining Philosophers applet – executing.

Figure 6.9: Dining Philosophers applet – deadlocked.

Chapter 7: Safety and Liveness Properties

Figure 7.1: ACTUATOR LTS.

Figure 7.2: property POLITE.

Figure 7.3: property CALM.

Figure 7.4: Single-lane bridge.

Figure 7.5: SingleLaneBridge model.

Figure 7.6: Single-lane bridge class diagram.

Figure 7.7: Single-lane bridge display using Bridge class.

Figure 7.8: COIN model.

Figure 7.9: TWOCOIN model.

Figure 7.10: Action priority.

Figure 7.11: CongestedBridge model with two cars.

Figure 7.12: CongestedBridge model with one car.

Figure 7.13: READWRITELOCK LTS.

Figure 7.14: READERS_WRITERS model.

Figure 7.15: RW_PROGRESS LTS.

Figure 7.16: Readers–Writers applet display.

Chapter 8: Model-Based Design

Figure 8.1: Cruise control system.

Figure 8.2: Hardware constraints.

Figure 8.3: Structure diagram for the cruise control system.

Figure 8.4: Model for the cruise control system.

Figure 8.5: LTS diagram for INPUTSPEED.

Figure 8.6: LTS diagram for SPEEDCONTROL.

Figure 8.7: CONTROL trace.

Figure 8.8: LTS diagram for the property CRUISESAFETY.

Figure 8.9: Minimized LTS diagram for CONTROLMINIMIZED.

Figure 8.10: Minimized LTS diagram for the revised CONTROLMINIMIZED.

Figure 8.11: Design architecture, behavior model and other models.

Figure 8.12: Cruise control applet display.

Figure 8.13: Cruise control class diagram.

Chapter 9: Dynamic Systems

Figure 9.1: Golf Club applet display.

Figure 9.2: Golf Club class diagram.

Figure 9.3: ALLOCATOR LTS for N = 2.

Figure 9.4: PLAYER LTS for N = 2.

Figure 9.5: GOLFCLUB composition.

Figure 9.6: Golf Club applet with fair allocation.

Figure 9.7: Golf Club with bounded overtaking allocator (bound = 3).

Figure 9.8: join() demonstration applet.

Figure 9.9: MASTER_SLAVE LTS.

Chapter 10: Message Passing

Figure 10.1: Synchronous message-passing channel.

Figure 10.2: Synchronous message-passing applet display.

Figure 10.3: Modeling synchronous message passing.

Figure 10.4: SyncMsg labeled transition system.

Figure 10.5: Car park model.

Figure 10.6: Asynchronous message-passing port.

Figure 10.7: Asynchronous message-passing applet display.

Figure 10.8: APORT labeled transition system.

Figure 10.9: Asynchronous message applet model.

Figure 10.10: Rendezvous message-passing protocol.

Figure 10.11: Rendezvous message-passing applet display.

Figure 10.12: Rendezvous applet model.

Figure 10.13: Message-passing classes.

Chapter 11: Concurrent Architectures

Figure 11.1: Primes Sieve process architecture.

Figure 11.2: Minimized PRIMES LTS.

Figure 11.3: Minimized PRIMESUNBUF LTS.

Figure 11.4: Minimized AFILTER LTS.

Figure 11.5: Primes Sieve applet display.

Figure 11.6: Primes class diagram.

Figure 11.7: Supervisor – Worker process architecture.

Figure 11.8: TUPLE LTS.

Figure 11.9: SUPERVISOR and WORKER LTS.

Figure 11.10: Trace of Supervisor – Worker model.

Figure 11.11: Rectangle method.

Figure 11.12: Supervisor – Worker applet.

Figure 11.13: Supervisor – Worker class diagram.

Figure 11.14: Announcer – Listener process architecture.

Figure 11.15: LTS for a:REGISTER.

Figure 11.16: ANNOUNCER_LISTENER trace.

Figure 11.17: EventDemo applet display.

Figure 11.18: EventDemo class diagram.

Chapter 12: Timed Systems

Figure 12.1: Discrete time and mouse clicks.

Figure 12.2: DOUBLECLICK LTS and traces.

Figure 12.3: Timed Producer – Consumer deadlock.

Figure 12.4: LTS for OUTPUT (1,3).

Figure 12.5: LTS for JITTER(2).

Figure 12.6: LTS for RECEIVER(2).

Figure 12.7: Parcel router device.

Figure 12.8: Parcel router model structure.

Figure 12.9: STAGE structure.

Figure 12.10: Animation trace for STAGE(0).

Figure 12.11: Parcel router applet display.

Figure 12.12: Parcel router classes and interfaces.

Figure 12.13: Space Invaders applet display.

Figure 12.14: Game space.

Figure 12.15: Sprite and SpriteCanvas classes.

Figure 12.16: CollisionDetector class diagram.

Figure 12.17: SpaceInvaders class diagram.

Chapter 13: Program Verification

Figure 13.1: Sequential process BOMB.

Figure 13.2: Sequential composition LOOP.

Figure 13.3: Sequential composition and recursion.

Figure 13.4: Parallel composition of sequential processes.

Figure 13.5: WAITSET trace for notify.

Figure 13.6: WAITSET trace for notifyAll.

Figure 13.7: LTS for property BUFFER.

Chapter 14: Logical Properties

Figure 14.1: MUTEX property process.

Figure 14.2: Büchi automaton for FIRSTRED.

Figure 14.3: CongestedBridge showing acceptance states.

Figure 14.4: REDCROSS Büchi automaton.

Figure 14.5: REDEXIT Büchi automaton.

Figure 14.6: POLITE Büchi automaton.

Figure 14.7: POLITE_W safety property process.

Figure 14.8: SEQ property process.

Figure 14.9: Database ring architecture.