Notes and Further Reading


The use of state machines as an abstract model for processes is widely used in the study of concurrent and distributed algorithms. For example, in her book Distributed Algorithms, Nancy Lynch (1996) uses I/O automata to describe and reason about concurrent and distributed programs. I/O automata are state machines in which input, output and internal actions are distinguished and in which input actions are always enabled (i.e., they are offered as a choice to the environment in all states). The interested reader will find an alternative approach to modeling concurrent systems in that book.

State machines are used as a diagrammatic aid (usually as State Transition Diagrams, STD) in most design methods to describe dynamic activity. They can be extended to cater for concurrency. An interesting and widely used form is statecharts (Harel, 1987), designed by David Harel and incorporated in the STATEMATE software tool (Harel, Lachover, Naamad, et al., 1990) for the design of reactive systems. A form of this notation has been adopted in the Unified Modeling Language, UML, of Booch, Rumbaugh and Jacobson (1998). See http://www.uml.org/.

The association of state machines with process algebra is due to Robin Milner (1989) who gives an operational semantics for a Calculus of Communicating Systems (CCS) using Labeled Transition Systems in his inspirational book Communication and Concurrency. While we have adopted the CCS approach to semantics, the syntax of FSP owes more to C.A.R. Hoare’s CSP presented in Communicating Sequential Processes (1985). The semantic differences between FSP and its antecedents, CCS and CSP, are documented and explained in succeeding chapters. The syntactic differences are largely due to the requirement that FSP be easily parsed by its support tool LTSA.

Process algebra has also been used in formal description languages such as LOTOS (ISO/IEC, 1988). LOTOS is an ISO standard language for the specification of distributed systems as interacting processes. As in FSP, process behavior is described using action prefix and choice operators, guards and recursion. However, unlike FSP, LOTOS includes facilities for defining abstract data types. Naive use of the data type part of LOTOS quickly leads to intractable models.

FSP was specifically designed to facilitate modeling of finite state processes as Labeled Transition Systems. LTS provides the well-defined mathematical properties that facilitate formal analysis. LTSA provides automated support for displaying and animating the examples in this chapter. Later in the book we will see how LTSA can be used for verifying properties using model checking.

The reader interested in more details on Java should consult the information on-line from JavaSoft. For more on the pragmatics of concurrent programming in Java, see Doug Lea’s book Concurrent Programming in Java™: Design Principles and Patterns (1999).




Concurrency(c) State Models & Java Programs
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net