Second Edition | Concurrency: State Models and Java Programs

This second edition of the book provides the following main additions:

Dynamic Systems.

A new model and implementation for bounded dynamic resource allocation is presented and discussed in Chapter 9.
A new chapter on Program Verification.

The general approach used in the book is model-based design, where models are developed and analyzed before implementation. This chapter describes how concurrent implementations in Java can be modeled and verified. This is illustrated using examples from previous chapters.
Sequential process composition.

Processes are generally composed using parallel composition to model interaction and concurrency. Composition is extended to include sequential composition as well, thereby extending the ways in which models can be specified and analyzed.
A new chapter on Logical Properties.

The formalism used in the book is based on the identification and specification of events and actions rather than states. This chapter introduces the use of fluents and abstract states as a means of specifying logical, state-based properties in an event-based formalism. This extension supports property specification using Linear Temporal Logic (LTL). In addition to the provision of counterexamples in the case of property violations, witnesses can be provided to give examples of acceptable executions. This is illustrated using examples, both new and from previous chapters.
Extensions to LTSA.

Tool support for model analysis using LTSA has been extended to provide a number of additional features. These include a revised user interface, on-the-fly safety and progress analysis allowing complete analysis of much larger state spaces, approximate safety analysis using Holtzmann’s SuperTrace algorithm for larger state spaces, support for sequential composition, support for graphic animation, no limit on potential statespace (previously 2**63), and Partial Order Reduction during composition and analysis.
Java platform.

The demonstration programs and examples have been updated to use the new Java version which includes generic classes.