Flylib.com
List of Figures
Previous page
Table of content
Next page
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.
Previous page
Table of content
Next page
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162
Authors:
Jeff Magee
,
Jeff Kramer
BUY ON AMAZON
Identifying and Managing Project Risk: Essential Tools for Failure-Proofing Your Project
Identifying Project Scope Risk
Identifying Project Resource Risk
Monitoring and Controlling Risky Projects
Conclusion
Appendix A Selected Detail From the PERIL Database
Developing Tablet PC Applications (Charles River Media Programming)
Introduction to the VB .NET Language
Object-Oriented Programming with VB .NET
Creating an MP3 Player
Using Gestures to Control Tablet Media Player
Virtual Joystick
MySQL Cookbook
Specifying Which Rows to Select
Telling MySQL How to Display Dates or Times
Using a Join to Create a Lookup Table from Descriptive Labels
Identifying and Removing Unattached Records
Using Transactions in Java Programs
.NET-A Complete Development Cycle
GDI+ Programming
Requirements for Image Postprocessing Components
Performance Optimization, Multithreading, and Profiling
Design of the Optimizations
References for Further Reading
Programming .Net Windows Applications
The .NET Framework
Building and Running
TreeView
Custom Controls
Updating ADO.NET
DNS & BIND Cookbook
Pointing a Domain Name to a Particular URL
Dividing a Large named.conf File into Multiple Files
Configuring Multiple Mail Servers in DNS
Sorting Multiple Addresses in a Response
Configuring a Name Server to Listen for Queries on an IPv6 Interface
flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net
Privacy policy
This website uses cookies. Click
here
to find out more.
Accept cookies