An Overview of PROMELA
- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
This chapter is from the book
This chapter is from the book
This chapter is from the book
“What we see depends on mainly what we look for.”
—(Sir John Lubbock, 1834–1913)
In the last chapter we saw that the emphasis in PROMELA models is placed on the coordination and synchronization aspects of a distributed system, and not on its computational aspects. There are some good reasons for this choice. First, the design and verification of correct coordination structures for distributed systems software tends to be much harder in practice than the design of a non-interactive sequential computation, such as the computation of compound interest or square roots. Second, the curious situation exists that the logical verification of the interaction in a distributed system, though often computationally expensive, can be done more thoroughly and more reliably today than the verification of even the simplest computational procedure. The specification language we use for systems verification is therefore deliberately designed to encourage the user to abstract from the purely computational aspects of a design, and to focus on the specification of process interaction at the system level.
As a result of this specialization, PROMELA contains many features that are not found in mainstream programming languages. These features are intended to facilitate the construction of high-level models of distributed systems, The language supports, for instance, the specification non-deterministic control structures; it includes primitives for process creation, and a fairly rich set of primitives for interprocess communication. The other side of the coin is that the language also lacks some features that are found in most programming languages, such as functions that return values, expressions with side effects, data and functions pointers, etc. The reason is simple: PROMELA is not a programming language. PROMELA is a language for building verification models.
A verification model differs in at least two important ways from a program written in a mainstream programming language such as Java or C.
-
A verification model represents an abstraction of a design that contains only those aspects of a system that are relevant to the properties one wants to verify.
-
A verification model often contains things that are typically not part of an implementation. It can, for instance, include worst-case assumptions about the behavior of the environment that may interact with the modeled system, and, most importantly, it either explicitly or implicitly contains a specification of correctness properties.
Even though it can be attractive to have a single specification that can serve as both a verification model and as an implementation of a system design—verification and implementation have some fundamentally different objectives. A verification model is comparable in its purpose to the prototype or design model that a civil engineer might construct: it serves to prove that the design principles are sound. Design models are normally not expected to be part of the final implementation of a system.
A full system implementation typically contains more information, and far more detail, than a design model. This means that it can be difficult to find automatic procedures for converting design models into system implementations. The reverse, however, is not necessarily true. In Chapter 10 we will explore means for mechanically extracting the main elements of a verification model directly from an implementation, guided by abstraction techniques. Similarly, in Chapter 17 we will discuss the specific constructs that are available in PROMELA to facilitate model extraction tools. These topics, though, should be considered advanced use of the model checker, so we will conveniently ignore them for now.
In the last chapter we gave a bird’s-eye view of the language, briefly touching on some of the main language constructs that are available to build verification models. In this chapter we cover the language more thoroughly. We will try to cover all main language features in a systematic way, starting with the most general constructs, and slowly descending into more of the specifics. We restrict ourselves here to the mechanisms that are at our disposal for describing process behavior and process interaction. In the next chapter we will continue the discussion with a description of the various means we have to define correctness claims. After we have covered these basics, we move on in Chapter 5 to discuss methods for exploiting design abstraction techniques as an aid in the control of verification complexity.
First then, our overview of the basic language for specifying the behavior of concurrently executing, and potentially interacting, processes in a distributed system.
Types of Objects
PROMELA derives many of its notational conventions from the C programming language. This includes, for instance, the syntax for boolean and arithmetic operators, for assignment (a single equals) and equality (a double equals), for variable and parameter declarations, variable initialization and comments, and the use of curly braces to indicate the beginning and end of program blocks. But there are also important differences, prompted by the focus in PROMELA on the construction of high-level models of the interactions in distributed systems.
A PROMELA model is constructed from three basic types of objects:
-
Processes
-
Data objects
-
Message channels
Processes are instantiations of proctypes, and are used to define behavior. There must be at least one proctype declaration in a model, and for the model to be of much use there will normally also be at least one process instantiation.
A proctype body consists of zero or more data declarations, and one or more statements. The semantics of statement execution is somewhat special in PROMELA, since it also doubles as the primary mechanism for enforcing process synchronizations. We have seen some of this in the last chapter, and we will return to it in more detail in the section on executability (p. 51).
Process types are always declared globally. Data objects and message channels can be declared either globally, that is, outside all process type declarations, or locally, that is, within a process type declaration. Accordingly, there are only two levels of scope in PROMELA: global and process local. It is, for instance, not possible to restrict the scope of a global object to only a subset of the processes, or to restrict the scope of a local object to only part of a proctype body.
The next three sections contain a more detailed discussion of each of the three basic types of objects in PROMELA. This is followed by a discussion of PROMELA’s rules for executability, and a more comprehensive overview of the primitives in PROMELA for defining flow of control.