How to Document Behavior: Notations and Languages

How to Document Behavior Notations and Languages

Any language that supports documenting system behavior must include constructs for describing sequences of interactions. Because a sequence is an ordering in time, it should be possible to show time-based dependencies. Sequences of interactions are displayed as a set of stimuli and the triggered activities are ordered into a sequence by line, numbering, or ordering. Examples of stimuli are the passage of time and the arrival of an event. Examples of activities are computing and waiting. Languages that show time as a pointfor example, timeoutand time as an intervalsuch as wait for 10 secondsare normally also provided. As documentation of behavior implicitly refers to structure and uses structure, the structural elements of a view are an essential part of the language. In most behavioral documentation, therefore, you can find representations of

• Stimulus and activity
• Ordering of interactions
• Structural elements with some relationships the behavior maps to

Two groups of behavioral documentation are available, and the languages to support behavioral documentation tend to fall into one of two corresponding categories: traces and static models.

ADVICE

Use trace-oriented documentation if the goal is to analyze a difficult situation or to understand how the system behaves in a specific scenario.

• One type of documentation traces what happens through the structural elements of a system during a scenario. Those traces are complete only with regard to what happens in a system when a specific stimulus arrives while the system is in a specific state. Traces are by no means a complete behavioral model of a system. However, the union of all possible traces would generate a complete behavioral model, although this isn't remotely feasible in most systems. Traces are easier to design and communicate because they have a narrow focus.
• Another type of documentation, often state based, shows the complete behavior of a structural element or a set of elements. This is referred to as a static model of behavior because it is possible to infer all possible traces through a system, given this type of documentation. Static behavioral models support documentation of alternatives and repetitions to provide the opportunity of following different paths through a system, depending on runtime values. With this type of documentation, it is possible to infer the behavior of the elements for the arrival of any possible stimulus.

ADVICE

Use the static model type of documentation when a complete behavioral understanding is required, as is the case when performing a simulation or when applying static analysis techniques.

Not surprisingly, traces and static models document the behavior of elements in a system to different extents. In the documentation of a static behavioral model of a particular element, you typically find all the resources identified in the interfaces of that element: the complete behavior of the element. In the documentation of a trace, however, you find only the resources identified in the element interfaces that are involved in the execution of that particular scenario.

Another difference between the two approaches is the focus of the documentation relative to individual elements. Traces are typically scoped to include all the system elements that are involved in a particular scenario. However, as mentioned earlier, only a fraction of the behavior of any given element shows up in any particular trace. Each static model, on the other hand, is typically scoped to focus on all the behavior of a particular element. In order to reason about systemwide behavior, you must look at multiple static models side by side.

Many languages and notations are available for both types of behavioral documentation. These differ in the emphasis that is put on certain aspects of the behavior, such as how ordering is identified, how much support is available for documenting timing, what types of communication are easily modeled, and so on.

In the sections that follow, we provide cursory overviews of several notations within each of these categories. The discussions are intended to provide a flavor of the particular notations and to motivate their use. There are many ways in which the diagrams we present in this section may be used together to support the design process. Figure 8.1 shows a reasonable way to combine the strengths of several notations during the design processes.

Figure 8.1. Using various types of behavioral documentation together. Begin by documenting functional requirements with use cases (a), which helps clarify and understand the requirements and the system boundaries. Then produce use case maps (b) to document how the use cases work their way through the elements of the system. Next, produce sequence diagrams (c) from the use case maps to define the messages between the elements. Finally, once the message interfaces between elements are understood, produce statecharts (d) to completely document the behavior of the elements.

Each of the following notation sections is presented in terms of a common example, JavaPhone, an example meant to facilitate the development of telecommunication-aware applications on any platform supporting the standard. The JavaPhone example documents resources available for use in telephony, data communication, power management, and many other areas. We focus on a small portion of JavaPhone: making a point-to-point connection, or placing a call.

8.5.1 Traces

Traces are sequences of activities or interactions that describe the system's response to a specific stimulus when the system is in a specific state. These sequences document the trace of activities through a system described in terms of its structural elements and their interactions. Although it is conceivable to describe all possible traces through a set of elements to generate the equivalent of a static behavioral model, it is not the intention of trace-oriented documentation to do so. This would reduce the benefit of being readily comprehensible, owing to the resultant loss of focus.

In this section, we describe five notations for documenting traces: use cases, use case maps, sequence diagrams, collaboration diagrams, and message sequence charts. Although other notations are available, we have chosen these five as a reasonably representative sample of various types of trace-based notations.

Use Cases

A use case is a description of a unit of functionality performed by a single element. The functionality is described by documenting the sequence of interactions in which the element engages in order to provide the functionality. All interactions in a use case are interactions between the element and actors in its environment; no interactions within the element are shown. Use cases often include variants of the main sequence of interactions in order to document exceptional conditions.

Use cases are frequently used to capture initial requirements for a system by producing a use case for each system requirement. The element in these use cases represents the system itself, and each interaction is an interaction with an actor in the system's environment.

UML does not define any set notation for documenting use cases, but notations used in practice are generally brief and textual. Figure 8.2 uses one such ad hoc notation used to document a use case for JavaPhone.

Figure 8.2. Example use case for JavaPhone in an informal notation. This use case contains a main flow of events and one exceptional flow of events.

Use Case Maps

The use case map notation was developed at Carleton University and has been used to document and to understand a wide range of applications since 1992. Use case maps concentrate on visualizing execution paths through a set of elements from a bird's-eye view. The fairly intuitive notation helps communicate how a system works or is supposed to work, without getting lost in too much detail.

Use case maps can be derived from informal requirements or from use cases, if they are available. Responsibilities need to be stated or be inferred from these requirements. Separate use case maps can be created for individual system functionalities or even for individual scenarios. However, the strength of this notation resides mainly in the integration of related scenarios. In such cases, use case maps can be used to illustrate concurrency, such as resource contention problemsmultiple paths using one elementor possible deadlock situationstwo paths in opposite directions through at least two of the same elements.

If you ever followed a discussion of developers trying to answer concurrency-related questionsDoes an element need to be locked? Is there potential for deadlock?you may have seen them drawing pictures like the sketch in Figure 8.3. This type of informal notation is useful in answering such questions and illustrates a need for the well-defined equivalent found in use case maps.

Figure 8.3. Informal sketch of activities through some elements. The circles denote system elements; each line is a path of activity involved in a scenario.

The basic idea behind use case maps is captured by the phrase "causal paths cutting across organizational structures." An execution path in a use case map is just that; it describes how elements are ordered according to the responsibilities they carry out. When it enters an element, a box, an execution path, or line, states that now this element does its part to achieve the system's functionality. A responsibility that is assigned to the path while within an element defines it as a responsibility of the element.

Figure 8.4 shows an example JavaPhone use case map that deals with establishing a point-to-point connection. Use case maps include a means to represent execution path decomposition, allowing step-by-step understanding of more and more details of the system. Figure 8.4 includes an example of this. The Callee service stub, shown in the Root use case map with a diamond-shaped symbol, can be decomposed into either of the other use case mapsCallee service: Basic call or Callee service: Call forwarding. In this specific case, the decomposition is showing variation. The use case map notation includes many other symbols for such features as timers and timeouts, data containers, interactions between execution pathsabortingand goals, which are very useful when describing agent-oriented elements.

Figure 8.4. A use case map for JavaPhone. Execution paths are represented as sets of curvy lines. Execution paths have a beginning (large dot) and an end (thick straight line). Execution paths can split to show concurrent activities; they can be independent or join together again. Responsibilities assigned to a path are shown as annotated crosses on that path, and each is labeled in this example as Rn. The Root use case map contains two execution paths: one starting with connect and proceeding through Call with responsibility R1, and one starting with answer (TC2) and proceeding through the second Terminal Connection instance (TC2) with responsibility R4. Decomposition and variation are shown using a stub (diamond-shaped symbol) in the parent use case map, with incoming and outgoing execution paths. Child use case maps (Callee service: Basic call and Callee service: Call forwarding in this example) document in more detail what happens within the stub. In this example, the Callee service stub can be decomposed into either of the child use case maps, depending on the circumstances.

Sequence Diagrams

Sequence diagrams document a sequence of interactions, presenting a collaboration in terms of instances of elements defined in the structural documentation with superimposed interactions arranged in time sequence. In particular, a sequence diagram shows only the instances participating in the scenario being documented. A sequence diagram has two dimensions: vertical, representing time, and horizontal, representing the various instances. In a sequence diagram, relationships among the objectslike those found in a module vieware not shown.

Sequence diagrams support picturing dependent interactions, showing which stimulus follows another stimulus. Sequence diagrams are not very explicit in showing concurrency, however. Although a sequence diagram shows instances as concurrent units, no assumptions can be made about ordering when a sequence diagram depicts an instance sending messages at the "same time" to different instances or, conversely, receiving multiple stimuli at the "same time."

It might be intended that the interactions shown in different sequence diagrams can be performed independently of one another. If this is the intention when documenting behavior using sequence diagrams, it should be noted somewhere. It is not appropriate to document independent behaviors within the same sequence diagram.

Figure 8.5 shows a very simple, UML sequence diagram.

Figure 8.5. A UML sequence diagram. Instances have a "lifeline," drawn as a vertical line along the time axis. A lifeline can exist from the top of the time axis to indicate that an instance existsinstance ob1 of type C1when the scenario begins. Or a lifeline can begin and end to show creation and destruction of an instanceinstance ob2. The arrow labeled op depicts the message that creates instance ob2. A stimulus is shown as a horizontal arrow. The direction of the arrow defines the producerstart of the arrowand the consumerend of the arrowof the stimulus. A stimulus usually has a name. The name describes the stimulus and usually maps to a resource in the interface of the consumer instance. A stimulus can be drawn as a dotted line to indicate that it describes a return of control to the sender.

Figure 8.6 shows a more interesting sequence diagram, one that documents a portion of our running JavaPhone example. UML's sequence chart notation supports more features than we have illustrated. For example, interactions can be documented using different types of arrows to indicate more specific semantics for the communication (e.g., synchronous, asynchronous, periodic, and aperiodic types of communication). There are also ways to depict forms of flow control (e.g., decisions and iteration).

Figure 8.6. A UML sequence diagram for JavaPhone. A lifeline is shown as a vertical line to indicate the period during which the instance is active. The vertical ordering of interactions shows their relative ordering in time. Vertical distances between interactions may describe time duration in the sense that a greater distance stands for a longer time. However, this is not part of the standard UML semantics for sequence diagrams, and so any such use must be explicitly indicated. An informal extension to standard UML sequence diagrams is included; the answer interaction is shown without a source instance. This indicates that the interaction originates from the environment of the collection of elements found in the sequence diagram.

A constraint language, such as UML's Object Constraint Language (OCL), can be used to add more precise definitions of conditions like guard or iteration conditions. OCL statements can be attached to the arrow and become recurrence values of the action attached to the stimulus. A return arrow departing the end of the focus of control maps into a stimulus that (re)activates the sender of the predecessor stimulus.

Collaboration Diagrams

Like other trace notations, a collaboration diagram shows ordered interactions among elements needed to accomplish a purpose. Whereas a sequence diagram shows order using a time-line-like mechanism, a collaboration diagram shows a graph of interacting elements and annotates each interaction with a number denoting order. Instances shown in a collaboration diagram are instances of elements described in the accompanying structural documentation. Collaboration diagrams are useful when the task is to verify that an architecture can fulfill the functional requirements. The diagrams are not useful if the understanding of concurrent actions is important, as when conducting a performance analysis.

A collaboration diagram also shows relationships among the elements, called links (see Figure 8.7). Links show important aspects of relationships among those structural instances. Links between the same instances in different collaboration diagrams can show different aspects of relationships between the same structural elements. Links between instances have no direction. A link simply states that the connected instances can interact. If a more accurate definition is required, additional documentation elementsperhaps textual descriptionhave to be introduced.

Figure 8.7. A UML collaboration diagram for JavaPhone. Interactions are shown by using labeled arrows attached to linksthe linesbetween the instances, or boxes. The direction of the arrow identifies the sender and the receiver of each interaction. Special types of arrows, such as a half-headed arrow, can be used to depict different kinds of communication, such as asynchronous, synchronous, and timeout. Sequence numbers can be added to interactions to show which interactions follow which. Subnumbering can be used to show nested stimuli and/or parallelism. For example, the interaction with a sequence number 2.1a is the first stimulus sent as a result of receiving stimulus number 2. The letter a at the end means that another stimulus, 2.1b, can be performed in parallel. This numbering scheme may be useful for showing sequences and parallelism, but it tends to make a diagram unreadable.

Collaboration diagrams and sequence diagrams express similar information. Sequence diagrams show time sequences explicitly, making it easy to see the order in which interactions occur; collaboration diagrams indicate ordering by using numbers. Collaboration diagrams show element relationships, making it easy to see how elements are statically connected; sequence diagrams do not show these relations if connected elements do not interact in the scenario depicted in the sequence diagram.

Message Sequence Charts

A message sequence chart is a message-oriented representation containing the description of the asynchronous communication between instances. Simple message sequence charts look like sequence diagrams, but have a more specific definition and have a richer notation. The main area of application for a message sequence chart is as an overview specification of the communication behavior among interacting systems, especially telecommunication switching systems.

Message sequence charts may be used for requirement specification, simulation and validation, test-case specification, and system documentation. They allow documentation of traces through the system in the form of a message flow. A big advantage of a message sequence chart is that it defines a textual notation in addition to its graphical notation. This allows a more formalized model that can generate test cases that test an implementation against its specification.

Message sequence charts are often seen in conjunction with specification and description language (SDL), discussed later in this chapter. Whereas a message sequence chart focuses on representing the message exchange between elements, such as systems and processes, SDL focuses on documenting what does or should happen in an element. In that respect, message sequence charts and SDL diagrams complement each other.

Although message sequence charts look similar to sequence diagrams, they are used for different purposes. A sequence diagram is systemcentric in that it is used to track a scenario through the system, showing which elements are involved and how. A message sequence chart is elementcentric, and focuses on one element and how it interacts with its environment, without regard to the identity of other elements.

The most fundamental language constructs of message sequence charts are instances, or elements, and messages describing communication events, or interactions. Figure 8.8 shows how the JavaPhone layer interacts with its environment in establishing a point-to-point connection. In a message sequence chart, communication with outside elements is shown by message flow from and to the frame that marks the system environment. Figure 8.8 also documents actionsAlert and Establish Connectionand the setting and resetting of a timer.

Figure 8.8. A message sequence chart for JavaPhone. An instance is shown as a box with a vertical line. Message flow is presented by arrows, which may be horizontal or with a downward slope to indicate the flow of time. Horizontal arrow lines may also be bent to indicate message crossing. The head of the message arrow indicates message consumption; the opposite end indicates message sending. Along the instance axis, a total ordering of the described communication events is assumed. Within a message sequence chart, the system environment is graphically represented by a frame, which forms the boundary of the diagram. Communication arrows from and to the frame show message exchange with elements outside the scope of the diagram.

The complete message sequence chart language has many other primitives, such as for local actions, timersset, reset, and timeoutprocess creation, and process stop. Furthermore, message sequence charts have a means to show decomposition and so can be used to construct modular specifications.

8.5.2 Static Models

Static models show the complete behavior of structural elements. Given this type of documentation, it is possible to infer all possible traces through a system. The state machine formalism is a good candidate for representing the behavior of architectural elements because each state is an abstraction of all possible histories that could lead to that state. Once a system is in a state, it doesn't matter how it got there, only that it is there; it will react to the occurrence of a given event in the same way, no matter the particular history of the system at the time the event occurs. Languages are available that allow you to also document the internal behavior of elements in terms of finite state machines and element-to-element interactions in terms of interprocess communication of various types. These languages allow you to overlay a structural description of the elements of the system with constraints on interactions and timed reactions to both internal and environmental stimuli.

In this section, we describe three state-based languages: statecharts, specification and description language (SDL), and Z. Although other languages are available, we have chosen these three because they allow you to describe the basic concepts of documenting behavior in forms that capture the essence of what you wish to convey to system stakeholders. The three are also used as base representations in tools that you are most likely to encounter. Each language has been incorporated into one or more development environments that allow you to design, simulate, and analyze your system early in the development process.

Statecharts

Statecharts, a graphical formalism developed by David Harel for modeling reactive systems, allow you to trace the behavior of your system, given specific inputs. Statecharts add a number of useful extensions to traditional state diagrams, such as the nesting of states, concurrency, and primitives to express communication among concurrent units. These extensions provide the expressive power to document behavior concisely and to effectively model abstraction and concurrency.

Statecharts extend the finite state machine formalism to support description of the transitions within a state in terms of nested states. The outer state is called the superstate; inner states, substates. The superstate defines the scope of a new statechart, and the substates are related by transitions, just as in a finite state machine. When the superstate is entered, the initial state within the superstate is also entered. Grouping substates into a superstate is often done to allow common behavior to be expressed concisely. Any behavior indicated at the superstate leveldepicted as transitions from the superstate boundary rather than from any specific substateapplies to all substates. A good use of this technique is to indicate common error handling or termination behavior. Figure 8.9 shows an example of this; the alerting, failed, and connected states within the Connection state are grouped into an unnamed superstate so that common disconnection behavior can be expressed.

Figure 8.9. A UML statechart for JavaPhone. Sequence is shown by transitions and denoted by a single-headed arrow leading from the source state to the target state. Each transition is labeled with the event causing the transition. Alternatively, a transition could be triggered by the satisfaction of a guard condition, which is bracketed. Whenever the guard condition evaluates as true, the transition occurs. Transitions can also have consequences, called actions. When an action is noted, it indicates that the event following the slash will be generated when the transition occurs. Concurrency is represented by grouping sets of states into superstates and separating the superstates by dotted lines.

States can be nested in a different way to express concurrency. If the substates are separated by a concurrency boundarya dotted linerather than by transitions, each substate is also entered whenever the superstate is entered. Typically, this form of nesting is combined with the first. For example, a top-level superstate is composed of two or more concurrent substates. Each of the concurrent substates is in turn a superstate to substates that are connected by transitions.

This is, in fact, exactly the pattern followed in Figure 8.9. The top-level superstate, JTAPI, is composed of the three concurrent substates Call, Connection, and Terminal Connection. Each of these three substates is in turn a superstate to numerous other states, such as idle, active, and inactive in the Call state, connected by transitions. In Figure 8.9, the default start for each substate is depicted by an arrow coming from the initial state: a solid black circle. Initially, Call is in the idle state. As soon as the connect event arrives, Call generates a create event for Connection: the Connection.create action, which transitions Connection into the idle state. From there, events are exchanged with the telecommunication platform, and a Terminal Connection is created. Terminal Connection receives events from the telecommunication platform, which lead to state changes. Those changes trigger state changes in Connection, which trigger state changes in Call. Ultimately, each concurrent state transitions to the end state, a solid black circle enclosed by another circle; for example, on reaching the inactive state, Call transitions to the end state.

With the introduction of concurrency to finite state machines came a need to express communication among states. For example, when an event generated in one concurrent substate is intended to cause a transition in another substate, it is useful to indicate which substate should consume the event. For example, in Figure 8.9, a create event within the Call state is generated and intended to be consumed by the Connection state; this is denoted by labeling the event as Connection. create. This type of communication among statecharts is also needed when documenting interactions between statechart models for different elements of a system.

The statechart in Figure 8.9 shows the states some of the JavaPhone objectsCall, Connection, and Terminal Connectioncan be in when a phone connection is established and disconnected. The statechart shown contains important states and transitions but is by no means complete.

Statechart notation contains many other features not mentioned here, such as means of expressing choice, timing, and history and has been incorporated in UML.

SDL

Specification and description language (SDL) is an object-oriented formal language defined by the International Telecommunications Union (ITU)Telecommunications Standardization Sector. The language is intended for the documentation of complex, event-driven, real-time, and interactive applications involving many concurrent elements that communicate by using discrete signals. The most common application is in the telephony area.

SDL is an accessible language that can be used in an environment that is constructed of tools that support documentation, analysis, and generation of systems. SDL's strength lies in describing what happens within a system. If the focus is on interaction between systems, then a message-oriented representation, such as message sequence charts, is more suitable. SDL specifications are often used in combination with message sequence charts to explore a system's behavior.

SDL uses a finite state machine formalism at its core to model behavior. Constructs for describing hierarchical structure and interelement behavior enhance the capability for modeling large-scale systems. Structure is described in terms of a hierarchy of blocks that are eventually refined into sets of processes, as shown in Figure 8.10. Flow of data and stimulation among blocks and processes are described as signals that travel over named channels. Signals are the means of communication between blocks and processes. Communication is asynchronous and is specified textually as an annotation attached to a communication channel. Signals are visible to other blocks/processes at lower levels in the hierarchy, not to enclose blocks or other blocks at the same level.

Figure 8.10. A hierarchical structure and inter-element behavior in SDL for JavaPhone. The structure of a system is decomposed into a hierarchy of named blocks. Blocks are sets of either other blocks or processes but not combinations of these.

Processes run concurrently and have no knowledge of one another's states. Processes can be instantiated at startup or while the system is running. The internal behavior of a process is documented using a finite state machine formalism resembling flowchart notation. SDL provides a rich set of flowchart symbols, some of which are used in Figure 8.11 to partially document how a Terminal Connection is formed.

Figure 8.11. Intraprocess behavior in an SDL flowchart for JavaPhone. The various shapes represent specific aspects of behavior, including state changes, receiving input and sending output, decision, and so on: and lines represent the flow from one activity to the next. Flow is read from top to bottom.

SDL supports user-defined data types and provides several predefined typesInteger, Real, Natural, Boolean, Character, Charstring, PId, Duration, and Timethat have expected meanings. Variables, user-defined data types, and constant data values can be declared.

The hierarchy of blocks provides a structural view of the system; the flow among the blocks and processes, combined with process flowcharts, document system behavior. Once these aspects have been documented, it is possible to simulate the system and to observe control and data flow through the system as signals pass from block to block and into processes, where they move through the flowchart model of process behavior. This type of simulation allows you to visibly check how your system will react to various stimuli.

Z

Z, pronounced "zed," is a mathematical language based on predicate logic and set theory. As a language for formal specification, Z is used to produce precise behavioral models and permits rigorous analyses, such as type checking, model checking, and proofs. Z models document what behavior a system must exhibit, without constraining how it must be implemented. Z does so by focusing on data and operations involving the data.

Systems are specified as collections of schemas. Each schema documents a portion of the system; the two basic types of schema are often referred to as state schema and operation schema. A state schema contains a set of variables and invariants over those variables, the allowable combinations of which are permissible states of the system. An operation schema documents an operation over the state schema, documenting when it is allowed, via preconditions, and what is true when it is completed, via state changes. A simple banking example illustrating these schema types is shown in Figure 8.12.

Figure 8.12. Z schemas for a bank account. Schema Account, a state schema, defines the state space of an account to consist of two integers; Z is the symbol for an integer. This schema also documents an invariant, namely, that the account actual_balance must be greater than or equal to minimum_balance. In schema Withdraw, an operation schema, the first line above the dividing bar indicates that it is an operation that changes the state of an Account, the D indicating a state change. The amount? integer indicates an input parameter to the operation. Below the dividing line, the variables from Account appear in two different forms, with and without an accent (). The form without an accent refers to the value of the variable before the operation begins; the form with an accent, to the value of the variable after the successful completion of the operation. The first line after the dividing line then is a precondition; it indicates that the operation can be completed only if enough money is in the account. The next two lines indicate the results, postconditions, of successfully completing the operation.

Schemas allow the designer and other users of the specification to focus on one aspect of the system at a time and can also be combined using schema calculus to create complete behavioral models. The language supports a compositional approach to development, providing increased tractability when documenting large systems.

For example, Figure 8.12 could easily be extended using Z's schema calculus to deal with different aspects of a withdrawal. An additional operation schema could be written that focuses only on PIN verification at an ATM, and this operation could be combined with the Withdraw operation to express more complex behavior.

Figure 8.13 shows how we might document the running JavaPhone example in Z. However, we have restricted the example to the type of information conveyed in the other languages in this chapter, and so the figure doesn't contain the same kind of detail as in Figure 8.12. Essentially, Figure 8.13 uses the Z language to document when interactions are al-lowed but on a per interaction basis.

Figure 8.13. Z schemas for JavaPhone. Outside of the two schemas, the Connection_State type is defined as an enumerated type. The Connection state schema has only one state variable of type Connection_State. Each interaction over a Connection is modeled as an operation schema. The operation schema for the Active interaction is shown. The precondition documents in which states Active is a valid interaction and in which state Connection will end as a result of the Active interaction.

We've provided only a flavor of Z. Many other constructs are available for specifying more complex data types and relationships. Description of the schema calculus is beyond the scope of this presentation, as are the details of Z type checking and proof techniques. Additionally, a number of extensions to the Z notation, like Object Z and TCOZ, deal with such concepts as object orientation.

Z is particularly useful when you want to prove correct behavior in all cases, as when developing safety-critical systems. Additionally, commercial tools are available supporting development based on Z. Many practitioners who are experienced in the use of the language consider Z an invaluable tool because of these strengths. However, the language Z includes a large set of symbols, and expressions are written in terms of predicate logic, making it difficult for some designers to warm up to.

Other Notations

Other notations are emerging but not widely used yet. Some are domain specific, such as MetaH, and others are more general, such as Rapide. MetaH was designed specifically to support the development of real-time, fault-tolerant systems. Its primary emphasis is on avionics applications, although it has also been used to describe other types of systems. MetaH can be used in combination with ControlH, which is used to document and to analyze hardware systems. When used in combination, the system supports analysis of stability, performance, robustness, schedulability, reliability, and security.

Rapide has been designed to support the development of large, perhaps distributed, component-based systems. Rapide descriptions are stated in a textual format that can be translated into a box-and-arrow diagram of a set of connected components. System descriptions are composed of type specifications for component interfaces and architecture specifications for permissible connections among the components of a system. Rapide is an event-based simulation language that provides support for the dynamic addition and deletion of predeclared components, based on the observation of specified patterns of events during the execution of the system.

The Rapide toolset includes a graphical design environment that allows a designer to describe and to simulate a system. The result of a Rapide simulation is a POSET, a partially ordered set of events that form a trace of execution of the system. The simulation and analysis tools support exploring the correctness and completeness of the architecture.