Home > Publications > Completeness and Consistency                                                                                 PDF Version PS Version

 Completeness and Consistency in Hierarchical State-Based Requirements

Mats P.E. Heimdahl
Michigan State University
Department of Computer Science, A-714 Wells Hall
East Lansing, Michigan 48824-1027


Nancy G. Leveson University of Washington Computer Science and Engineering, FR-35 Seattle, WA 98195


This paper describes methods for automatically analyzing formal, state-based requirements specifications for some aspects of completeness and consistency. The approach uses a low-level functional formalism, simplifying the analysis process. Statespace explosion problems are eliminated by applying the analysis at a high level of abstraction; i.e., instead of generating a reachability graph for analysis, the analysis is performed directly on the model. The method scales up to large systems by decomposing the specification into smaller, analyzable parts and then using functional composition rules to ensure that verified properties hold for the entire specification. The analysis algorithms and tools have been validated on TCAS II, a complex, airborne, collision-avoidance system required on all commercial aircraft with more than 30 passengers that fly in U.S. airspace.

1 Introduction

A software requirements specification should be a comprehensive statement of a software system's intended behavior. Unfortunately, requirements specifications are often incomplete, inconsistent and ambiguous. We know that many serious conceptual errors are introduced in this first stage of software development -- errors introduced during the requirements stage have been shown to be more difficult and more expensive to correct than errors introduced later in the lifecycle, and they are more likely than implementation errors to be safety critical [20, 21]. Therefore, it is important to provide methods and techniques to eliminate requirements-related errors as early as possible.

To provide analysis procedures to find errors in specifications, it is first necessary to determine the desirable properties of a specification. Previously, we defined formal criteria for requirements completeness, consistency and safety. Jaffe, in his dissertation, defined a rigorous basis for ascertaining whether or not a given set of software requirements is internally complete, i.e, closed with respect to statements and inferences that can be made on the basis of information included in the specification [17]. Emphasis is placed on aspects of requirements specification that are usually not adequately handled, including timing and robustness, and on aspects that are particularly related to safety and accidents.

The definition of specification completeness provided by Jaffe was subsequently formalized using a simple Mealy-machine model called RSM (Requirements State Machine) [16]. The RSM notation was developed solely as a means for formally defining our criteria, and lacks most desirable properties of a true requirements specification language. To be useful in practical applications, these criteria need to be translated into criteria applicable to a real specification language. Although the criteria could be applied to many languages, we chose to work with a formal, state-based specification language called RSML (Requirements State Machine Language). RSML was developed by the Irvine Safety Research Group using a real aircraft collision-avoidance system called TCAS II (Traffic alert and Collision Avoidance System II) as a testbed [19].

This paper describes an automated approach to analyzing an RSML specification for two qualities: (1) completeness with respect to a set of criteria related to robustness (a response is specified for every possible input and input sequence) and (2) consistency (the specification is free from conflicting requirements and undesired nondeterminism). The need for consistency is obvious, but the robustness criteria require further explanation.

Embedded software is part of a larger system and usually provides at least partial control over the system in which it is embedded. This type of software is often reactive in that it must react or respond to environmental conditions as reflected in the inputs arriving at the software boundary. A robust system will detect and respond appropriately to violations of assumptions about the system environment (such as unexpected inputs). Robustness with respect to a state-machine description implies the following:

  1. Every state must have a behavior (transition) defined for every possible input.
  2. The logical or of the conditions on every transition out of any state must form a tautology.
  3. Every state must have a software behavior (transition) defined in case there is no input for a given period of time (a timeout).

Thus, the software must be prepared to respond in real time to all possible inputs and input sequences. That is, the software must be complete with respect to its input domain. In the rest of this paper, we use the term d-complete to represent this aspect of requirements completeness.

Manually verifying compliance with our set of criteria is a time-consuming and errorprone process. Thus, tools that support automated verification would be highly desirable. This analysis, unfortunately, is computationally expensive and infeasible in most specification languages. To overcome this problem, the semantics of RSML was defined with analyzability as one of the main goals.

In order to accomplish our goal of analyzability, we view a specification expressed in RSML as a mathematical relation composed from simple, analyzable parts. The compositionality is achieved through the definition of the next-state relation and by enforcing some simple restrictions on the way in which a system can be modeled. The compositional approach allows us to split a large problem into small manageable partitions, perform the analysis on each separate piece, and then combine the individual analysis results into a statement about the entire system. Analysis procedures that are too costly to apply to the monolithic problem can then be applied to manageable subsets of the problem and the individual results combined to make a statement about the original problem.

Related approaches to requirements analysis include methods based on formal proof systems and different static analysis techniques such as reachability analysis and model checking.

Formal proof systems: Formal proof systems can be powerful tools in the verification of critical properties of algorithms [25]. Attempts have been made to extend the use of formal proofs and apply them to requirements specifications, for example, the ProCoS (Provably Correct Systems) project [23, 24]. Unfortunately, the languages used in the theorem proving approach, such as process algebras and higher order logics, are not understandable by the non-software professionals involved in most requirements specification efforts and thus are not suitable as high-level requirements languages. Also, formal proofs are notoriously difficult to derive, and these approaches may not be practical for complex systems.

Reachability analysis: Modeling a system as a finite-state machine and then performing reachability analysis of the global state space has been successfully used in the analysis of communication protocol specifications [8, 14, 15]. The main problem with reachability analysis is that it relies on the generation of a global reachability graph and, therefore, quickly runs into a state-space explosion problem.

Model checking: Model checking is conceptually simple and is applicable in a wide variety of languages and application areas [1, 6, 7]. Early work in model checking also relied on a global reachability graph. Consequently, the approach suffered from statespace explosion problems. Newer approaches relying on a symbolic representation of the state space can significantly improve the performance of the model checking approach [5]. Symbolic model checking has been applied to large models [5, 4], but only for systems with simple, repetitive elements -- such as those commonly found in hardware applications. The time and space complexity of the symbolic approach is affected not only by the size of the specification but also by the regularity of specification. Software requirements specifications lack this necessary regular structure, and it is unclear how well the symbolic approach will perform on these specifications. Model checkers are currently unable to handle as complex a software specification as the TCAS II requirements specification.

Our approach differs from these techniques in that it performs the analysis directly on a high-level requirements model without generating a global reachability graph. Thus, the analysis is both conceptually simple and eliminates the problem with state-space explosion. To ensure that the formal RSML specification language and the associated analysis algorithms and tools are appropriate for large and realistic systems, a testbed specification was developed for TCAS II [18]. The testbed is currently being used to develop and validate various types of analysis algorithms and tools on the underlying formal model. TCAS II has been described by the head of the TCAS program at the FAA as the most complex system to be incorporated into the avionics of commercial aircraft. It therefore provides a challenging experimental application of formal methods to a real system.

This paper documents our approach to static analysis of RSML and gives examples of the types of problems that d-completeness and consistency analysis are capable of detecting. Section 2 gives a short introduction to the features of RSML necessary to understand this paper. Section 3 provides a formal definition of these RSML features. The definition is based on the notion that a transition in a simple state machine can be viewed as a function mapping the current state to the next state and the behavior of a hierarchical state machine can be viewed as a composition of simple functions. Automated analysis procedures for d-completeness and consistency are outlined in Section 4. An evaluation of the algorithms and examples of the types of problems this analysis is capable of detecting is described in Section 5. Section 6 presents conclusions.

2 Overview of the RSML Notation

RSML is a state-based requirements specification language suitable for the specification of reactive systems. RSML includes several features developed by Harel for Statecharts [10, 9]: superstates, AND decomposition, broadcast communication, and conditional connectives. In addition, RSML has some unique syntactic and semantic features that were developed to enhance readability, reviewability, and analyzability and our ability to handle complex systems. A complete description of RSML is provided in [19]. This section contains only a description of the RSML features necessary to understand this paper.

A simple finite-state machine is composed of states connected by transitions (see Figure 1). Default or start states are signified by states whose connecting transition has no source. In Figure 1, state A is the start state. Transitions define how to get from one state to another. In Figure 1, states B and C are directly reachable from A. State D is only indirectly reachable from A via state C.

Figure 1: Basic State Machine

Basic State Machine

Figure 2: A superstate example

Superstate example

Superstates. In RSML (and Statecharts), states may be grouped into superstates (see Figure 2). Such groupings reduce the number of transitions by allowing transitions to and from the superstate rather than requiring explicit transitions to and from all of the grouped states (substates). Superstates can be entered in two ways. First, the transition to the superstate may end at the superstate's border (transition A in Figure 2). In this case, a default state must be specified within the superstate. In the example, state S is entered upon taking transition A. Alternatively, the transition may be made to a particular state inside the superstate (transition B in Figure 2). The same superstate may have transitions ending at the border and at any number of the inner states. The superstate may be exited in two ways (transitions C and D in Figure 2). Analogous to transitions into the superstate, transitions out of the superstate may originate from the border or from an inner state. The same superstate may contain both types of exiting transitions. Note that all transitions to and from the superstate boundary can be redrawn to cross the boundary and enter the substates explicitly (Figure 3).

Figure 3: Transitions re-drawn to bypass the superstate.

Re-drawn superstate example

AND Decomposition. One of the most important innovations in Statecharts is what Harel calls the parallel state. Parallel states are also known as "orthogonal products", "product states", and "AND states". Parallel states contain two or more state machines separated by dashed borders (Figure 4). When the parallel state S is entered, each of the state machines A, B, C, and D within it is entered. All state machines are exited when any transition is taken out of the parallel state. The use of parallel states greatly reduces the size of the specification. For example, we estimate that the TCAS system (i.e., the complete reachability graph) contains at least 1040 states, whereas the hierarchical state diagram in our RSML specification of TCAS has approximately 140 states and fits on five pages.

Figure 4: The parallel state.

The parallel state

Transition Definitions. Transition definitions in RSML contain five parts: (1) the identification (the source and destination of the transition), (2) the location, (3) the triggering event, (4) the guarding condition, and (5) the output action. The identification, location, and triggering event are the only required parts. Figure 5 shows the syntax of a transition definition in RSML.

Transitions are taken upon the occurrence of the trigger event, provided that the guarding condition is true. The guarding condition defines preconditions on the transition and is specified using AND/OR tables, described below. Output actions identify events that are generated when the transition is taken. These newly generated events may now trigger transitions elsewhere in the state machine.

Although specification languages such as Statecharts and RSML can be used for many purposes, RSML was explicitly designed to be used for pure black-box requirements specifications. Such specifications describe only the externally visible behavior of the system component being defined in terms of a model of the relationship (mathematical relation) between the inputs and outputs. In addition, RSML specifications describe this behavior (relation) only in terms of variables and conditions of objects external to the computer (the sensors, actuators, and system components controlled by the software).

Therefore, internal events in RSML specifications are used only for one very specific purpose: to order the evaluation of the mathematical (input/output) relation to be computed by the software. Basically, they serve the same purpose as parentheses in algebraic equations. Viewing an RSML specification as a mathematical relation is the basis for our formalization of the language and will be described in detail in Section 3.

AND/OR Tables. Statecharts use predicate calculus to describe the guarding conditions on the transitions [2, 9]. Our TCAS external reviewers (including avionics engineers, component engineers, airline representatives, and pilots), however, did not find this notation natural or reviewable. Instead, we decided to use a tabular representation of disjunctive normal form (DNF) that we call AND/OR tables (see Figure 5 for an example from the TCAS II requirements).

Figure 5: A transition definition from TCAS II.

Transition Definition

The far-left column of the and/or table lists the logical phrases. Each of the other columns is a conjunction of those phrases and contains the logical values of the expressions. If one of the columns is true, then the table evaluates to true. A column evaluates to true if all of its elements are true. A dot denotes "don't care."

The next section formally defines the structure of these basic syntactic features and gives a formal definition of the semantics of RSML based on the composition of mathematical functions.

3 A Functional Framework

The behavior of a finite-state machine can be formally defined using a next-state relation. In RSML, this relation is modeled by transitions and the sequencing of events. Thus, one can view a graphical RSML specification as the definition of the mathematical next-state relation F . If, however, the relation F behaved as a mathematical function, and it was defined over all possible system states, some highly desirable properties of requirements specifications would be satisfied:

bulletThe model M would have a response specified for every possible input (i.e., it would be d-complete ),
bulletThe model would have no conflicting requirements (i.e., it would be consistent), and
bulletThe model would be deterministic.

Thus, by forcing the behavior of an RSML specification to be a mathematical function, we can guarantee the d-completeness, consistency, and determinism of a requirements specification. This is really the essence of the difference between our approach and others. Instead of allowing the next-state relation to be defined in a way that makes the analysis procedures difficult and then working hard to find analysis procedures that will work on the resulting model, we limit F (the next-state relation) in the language semantic definition in a way that makes the analysis relatively easy. Our resulting analysis algorithms are simple and can be performed directly on the model without needing to generate any part of the reachability graph.

As a side benefit, during the TCAS specification development we found that this nextstate relation was easier for the reviewers to interpret correctly than the alternatives we tried (it seemed to satisfy their intuitive understanding of state machines better). In fact, we decided on this semantic definition before we discovered that it simplified the analysis. Perhaps this just confirms the hypothesis that has been occasionally raised that languages for which the formal semantic definitions are simple also seem to be the easiest for users to understand and use correctly.

It may seem overly restrictive to require that the behavior of the software be limited to a mathematical function. However, safety-critical software should not be incompletely specified. In [16], we define requirements completeness as the specification being sufficient to distinguish the behavior of the desired software from that of any other, undesired program that might be designed. Nondeterministic specifications often hide dangerous incompleteness in this sense. In this paper, we show a nondeterminism in the TCAS specification we found that was unplanned, had serious safety implications, and was not obvious to us when developing the specification. If one of several possible alternatives is preferable with respect to some desired system quality, then this decision needs to be made by application experts, not by the programmers or software engineers, and it should be made during the requirements analysis process rather than later. Identifying nondeterminism in the specification will help with this decision-making. If two behaviors are identical with respect to all desired system qualities (which is highly unlikely), there is still the problem of determining this equivalence. In most cases, it is easier to evaluate a single deterministic behavior for all desired qualities than to evaluate multiple behaviors for all required qualities. In addition, nondeterministic behavior is usually undesirable with respect to the human-machine interface.

This section provides a formal definition of the semantics of the basic features of RSML. Section 3.1 defines the static structure of the state hierarchies. Section 3.2 describes how the dynamic behavior defined by the transitions and events in RSML can be viewed as compositions of functions. Those readers primarily interested in the use of the analysis tools and not in the formal foundation might skip to Section 4.

3.1 Hierarchical State-Machines

An RSML state machine M can be described by a six-tuple: where:

S is a finite set of states. These states are used to model the global system states. It is important to note the difference between the elements of S (states) and the global state. Due to the hierarchical and parallel nature of the state machines, the global state is always described by a set of states.

σ is a function mapping a state onto a set of states (S ↣ 2S). This function defines the hierarchy relation (or parent/child relation) on the states. In the graphical notation, this relation is visualized as containment (states are contained within superstates). For example, in Figure 6 the state A contains the states {B, C, D, E} (σ(A) = {B, C, D, E}). σ is defined to be cycle free.

Figure 6: A sample state hierarchy

sample state hierarchy

Definition 1 The hierarchy function σ is defined by:


definition of

σ1(x) is in the remainder of this paper referred to as σ(x). This definition implies that σ*(x) contains {x} and all its descendants. σ+(x) does not contain {x}, only its descendants.

π is a partitioning function. π partitions the descendants of a state into disjoint sets. The partitions of a state's descendants must be mutually exclusive. In Figure 7, for example, π(A) partitions the descendants of A into two disjoint sets (π1(A) and π2(A)). In the graphical notation, this partitioning is denoted using dashed lines. Thus, C0;1(A) = {B, C} and π2(A) = {D, E}. The cardinality (kA) of A is in this case 2. It should be noted that x is a parallel state (AND state) if kx >= 2 and we refer to the different partitions of the descendants of x as parallel components. The partitions of a state's descendants are required to be mutually exclusive.

Figure 7: A sample state machine.

Sample State Machine

Definition 2 Let x,z ∈ σ(x). The partitioning function #x03C0; is defined by:

Informally, if σ(y) and σ(z) intersect, then y and z are equivalent.

V is a set containing the input and output histories of the model (the complete variable traces).

c0 is the initial global state of the machine, c0 ∈ (2S V). A global state is an ordered pair consisting of a set of states, known as the configuration of the machine, and a trace from V. The initial global state in Figure 6 is defined by the pair ({A, B, D}; ∅). The properties of a configuration are formally defined in Appendix A.

F is a relation defining the global state changes in the machine M (and the possible changes in the output variables). F is a mapping CI, where C ⊆ (2S &#x00D7 V). The relation F is also referred to as the behavior of M.

In the definitions above, there are few restrictions on the nature of a global state. All that is required is that a global state ci is an element of C. From the discussion in Section 2, it is clear that there are certain combinations of states that are not allowed when describing the global state. In Figure 7, for example, the states B and C cannot both be part of the global state, that is, the machine cannot be in the state B and the state C simultaneously. The restrictions governing the structure of a global state have been formally defined for Statecharts by Harel [11]. These definitions are also applicable to RSML. Although the definitions are not essential for understanding the remainder of the paper, for completeness they have been included in Appendix A.

The remainder of this section is devoted to the next-state relation F . We will show how the transitions in RSML can be viewed as mathematical functions and how these functions can be composed to form the complex behavior of the global next-state relation F.

3.2 Next-State Mapping

The hierarchies and parallelism (defined by the functions σ and π), together with the definitions in Appendix A, enforce a rigorous structure on the possible global states (the set C). The dynamic behavior (the possible global state changes) is defined by the next-state relation F (C ↣ C). In a model of a system with nontrivial functionality, this mapping will be complex. However, the mapping can be viewed as a composition of smaller, less complex mappings. Specifically, F can be viewed as composed of simple functions.

In the graphical notation, these simple functions are defined by transitions. The domain of a function is defined by the source, i.e., the state that the tail of the transition is leaving, and the guarding condition on the transition. The image of a function is defined by the destination of a transition, i.e., the state the transition enters, and possible output. The functions represented by the transitions are then composed depending on the structure of the particular state machine being considered and the events defined on the transition. The semantics of RSML are defined using three basic functional compositions:

Union: The union composition of two functions (g U h) merges the domains of the functions.

Definition 3 The functional properties are maintained under union (U) if

Union composition of two functions is allowed if the domains of the functions do not overlap, or the domains overlap but the functions are equivalent for all elements in the intersection. The notation Card(X) is used to denote the cardinality of X.

Serial: Serial composition g(h(c)) (or g ∘ h) corresponds to normal functional composition.

Definition 4 Serial composition (g ࢪ h) is allowed iff

Informally, serial composition is allowed if the image of the first function applied is a subset of the domain of the second function, i.e., the second function is defined for all possible results of the first function.

Parallel: Parallel application is denoted < h,g > (x). Parallelism is modeled as interleaving, i.e., an arbitrary ordering of functional applications.

Definition 5 Parallel composition is allowed iff

Parallel composition is allowed if both possible serial compositions are allowed. If g ∘ h(x) != h ∘ g(x), i.e., the ordering of the functional application is important, parallel composition will lead to nondeterminism and the properties of a function are lost.

In RSML, union composition occurs between nonparallel transitions triggered by the same event. For example, the functions representing the transitions t1, t2, and t3 in Figure 7 (assuming all are triggered by the same event) are composed in union.

Transitions triggered by the same event, but in parallel state components, are composed in parallel. In Figure 7, transitions t3 and t4 are composed in parallel (assuming they are triggered by the same event).

Finally, serial application is caused by the event propagation mechanism. Assume the transition t5 is triggered by some external event and generates event e as an action. This event is picked up by transition t6 -- that is, t6 is triggered by e. Thus t5 is the transition taken first and t6 second. This sequencing is modeled as applying the functions representing t5 and t6 in series: t6t5(c).

In this way the complete behavior of any model can be hierarchically defined as a composition of the behaviors of its parts.

Before we can define the complete behavior of an RSML specification, we have to investigate the nature of the functions defined by the transitions. A function can be textually defined by

where Qs and Qd are sets of states, x is a state, and p is an arbitrary predicate over the configuration c. In the graphical representation, this function represents a transition with the tail in the state x and the guarding condition p. If the transition is taken, the structure of the state machine may cause more states than x to be exited -- for example, if x is a superstate. The set of states that is exited when the transition is taken is denoted by Qs and the set that is entered by Qd. In the definition above, the set &#x007B c | (x &#x2208 c) &#x2227 p(c) &#x007D defines the domain of the function (Dom(f)), and Qs and Qd are the source (Source()) and destination (Dest()) of respectively.

The functional definition of a complete RSML specification is hierarchically built up from (composed of) the functional definitions of its components. We start by defining the behavior of the simplest possible state machine, that is, a state machine consisting of one state and no transitions. An atomic state (a state without descendants) that has no transitions is defined to have no behavior.

Definition 6 The behavior (g) of an atomic state a, i.e., σ(a) = ∅:

ga = ∅

The behavior of a set of states grouped in a parallel state component is defined as the union of (1) the behaviors of the states included in the component and (2) the functions introduced at this level of abstraction describing transitions between the states. The notation gC0;i denotes a function (transition) g intrfoduced in the parallel state component πi. In Figure 7, the function represented by t4 belongs to π1(A).

Definition 7 A function g belongs to the parallel component πj (denoted by gπj) iff:

Definition 8 The behavior of a parallel state component πi(s):

Informally, a parallel state component behaves either as one of its states, i.e., the state it is currently in, or according to the transitions between the states contained in the component.

The behavior of a composed state (a superstate) is defined as the parallel composition of its parallel state components. The set {1,....,ks} is an enumeration of the parallel state components into which σ(s) is partitioned. In Figure 7, for example, σ(A) is partitioned into four parallel state components.

Definition 9 The behavior of a composed state s, σ(s) != ∅:

Informally, one can view the components of the composed states as processes, and the behavior of the composed state as the parallel execution of these processes.

The rules defined above govern the behavior under one specific event, i.e., all transitions in the model triggered by this one event are composed according to these rules. The behavior for all individual events in the model can now be modeled in a similar way. If an event e is generated, the function defined by the behavior under e, i.e., the behavior generated by composing all transitions triggered by e, is applied, and a new system state is calculated. The only remaining part to model is the event propagation mechanism. Since output actions can be associated with transitions, they are also associated with functions. After a function has been applied and a new system state calculated, a new function is applied based on the output actions from the previous function.

The set of all functions with the output action a is denoted a, and the composed behavior of the state machine for event e is denoted Fe. The function defining the behavior of M under the event e must be applied after a function with the action e has been applied, i.e., ... Fe(e(...)).... The different possible compositions of functions defining F could be explicitly listed to define the complete behavior. Listing all the possible compositions is generally infeasible, however, and it is easier to define rules for how to combine the behaviors under individual events to form the complete behavior of M.

Definition 10 Let x 2 C. The Yield of a function application is defined as:

An evaluation of F is always started by the arrival of an input. A sequence of function applications will follow. This sequence will ultimately be terminated by the application of a function with no yield. The next function is always determined by the yield of the previous function.

Definition 11 The next function application is defined by:

Note that in order for the compositions defined in this section to maintain the properties of a function, all rules for serial and parallel composition defined in the beginning of Section 3.2 have to be followed.

4 Analysis Approach

If the relation F defining the dynamic behavior of the model is a function, then dcompleteness , consistency, and determinism are assured. By investigating the fairly simple compositions defining the dynamic behavior of the system, these properties can be evaluated.

The analysis approach is based on the compositional properties of the semantic definition. The base step in the analysis is to assure that transitions out of atomic states do not conflict and never leave the behavior undefined, i.e., the requirements are d-complete with respect to the individual atomic states. In this way, we can guarantee that if the model is in this state and an event triggering any transition out of the state is generated, a transition out is defined independently of the global state and the input that has arrived at the model boundary. The rules for union, parallel, and serial composition can then be applied to show that the behavior of the entire hierarchical and parallel machine is d-complete and consistent. That is, by only investigating the functional compositions, we can ensure that the d-completeness and consistency properties verified for a single state are not compromised by hierarchies, parallelism, and event propagation.

This section outlines algorithms analyzing a model for the satisfaction of functional properties.

Union Composition: Union composition requires that the domains of the functions describing the transitions involved in the composition are disjoint, i.e., no two transitions out of the same state can be satisfied at the same time. In addition, functions require that the entire domain is covered. Thus, there must be a satisfiable transition out of every state independent of what input arrives at the model boundary.

The guarding conditions on the transitions triggered by the same event are pairwise compared to see if they are mutually exclusive. Two transitions with guarding conditions that are not mutually exclusive represent conflicting requirements. In addition, if the logical or of the conditions on all transitions out of the state triggered by the same event does not form a tautology, then there are conditions for which no behavior is specified, i.e., the requirements are incomplete. Tables 1-3 outline the data structures and the algorithm used to analyze for d-completeness and consistency of individual states.

struct State {
   String name;
   State parent;
   StateList children;
   TransitionArray all_trans_out;

struct Transition {
  State source;
  State dest;
  Condition cond; // The guarding condition on the transition Event trigger;
  EventArray actions;
  InfoSet uses; // All elements in M this transition depends on InfoSet 
  effects; // All elements in M this transition effects 

Table 1: Data structures used to represent the state space

struct Conflict {
   Transition trans1;
   Transition trans2;
   Condition cond;

Table 2: Data structure for conflicting transitions

void Complete_Consistent_Under_e(State state, Event e) {
   Condition defined_for;
   defined_for = FALSE;
   for (int i = 0; i < size_of(state.all_trans_out); i++) {
      if (state.all_trans_out[i].trigger == e) {
         defined_for = defined_for || state.all_trans_out[i].cond;
   for (j = i; j < size_of(state.all_trans_out); j++) {
      if (state.all_trans_out[j].trigger == e) {
         conflict_condition = state.all_trans_out[i].cond &&
         if (conflict_condition != FALSE) {
            create a new conflict;
            conflict.trans1 = state.all_trans_out[i];
            conflict.trans2 = state.all_trans_out[j];
            conflict.cond = conflict_condition;
            Append(conflict_array, conflict);
   if (!defined_for) /* If there are no transitions
                        triggered by e */
      output("No transition out of the state" state "is satisfied");
      output("under the event" e "if" !defined_for);
   output("There are conflicts between the following transitions:");


In RSML, the conditions are represented by AND/OR tables (Figure 5). The conditions for state transition in TCAS II are quite complex, resulting in many cases in large tables and requiring costly logical AND and OR operations on the transitions (satisfiability of boolean functions is known to be an NP problem). Our analysis tools use Binary Decision Diagrams (BDDs) [3] for the manipulation of the conditions. BDDs are data structures used to represent boolean functions in a canonical form. Initially, our main concern was the performance of the AND and OR operations needed to check for mutual exclusion and complete coverage. With BDDs, Boolean formula manipulation can be performed in time linear to the size of the BDD structure. Unfortunately, in the worst case the size of the BDD structure is exponential in the number of terms in the boolean function it is representing. The BDD approach has provided excellent performance for all examples from TCAS we have tried. Since the BDDs manipulate predicates symbolically, the analysis is conservative and spurious error reports may be generated. This issue will be covered in more detail in Section 5.1.1.

Serial Composition: Serial application of functions arises out of the event propagation mechanisms provided in RSML (and Statecharts). A transition triggered by event e1 may generate event e2 as an action, i.e., if e1 occurs, the transition is taken and e2 is generated. The event e2 may now trigger another transition somewhere else in the model. If an event is generated but does not trigger any transition, it is likely that this event was generated in error or that transitions triggered by this event are missing from the requirements. Serial composition of functions requires that the image of the first function is a subset of the domain of the second function. In the graphical model, this requirement implies that if an event is generated, there must always be a transition elsewhere in the model ready to be triggered by this event. All states have a set of transitions enabled (or ready) that can be taken when the model is in a specific state. Using one bottom-up pass over the state hierarchy, all states can be annotated with the transitions enabled in them.

It is also possible to annotate each state with the states that can co-exist in the global state description. With this annotation, assuring that all events generated as actions will be used is straight forward.

Parallel Composition: Parallel composition occurs when two (or more) transitions in parallel state machines are triggered by the same event (or events generated simultaneously). If the truth value of the guarding condition of one transition can be affected by a state change caused by a parallel transition, then there exists a possibility of nondeterminism, and the transitions are said to conflict with each other.

A pairwise comparison of all parallel transitions can assure determinism: If no two transitions conflict, then the model is deterministic. Table 4 and 5 outline the data structures and algorithm used for this analysis. The pairwise comparison of all transitions existing in parallel and triggered by simultaneous events is potential costly; in the worst case (all transitions are parallel), the algorithm requires O(n2) comparisons (where n is the number of transitions in the model). Fortunately, the number of parallel transitions in real systems seems to be fairly limited, and this straight forward approach has been shown to be adequate to analyze a major part of a large real life system (TCAS II) for determinism [12].

struct Event {
   String name;
   TransitionArray transitions; // All transitions triggered by this event

struct Nondeterministic {
   Trans trans1;
   Trans trans2;

Table 4: Data structure for non-deterministic pairs of transition

NondeterministicArray NondeterministicTransitions(Event e) {
   NondeterministicArray resultArray;

   for(i = 0 ; i < size_of(e.transitions); i++) {
      for(j = i+1; j < size_of(e.transitions); j++) {
         if (parallel((e.transition[i]),
                      (e.transition[j])) &&
                        e.transitions[i].effects))) {
            AppendPair(result_array, e.transition[i],
   return resultArray;

Table 5: Determinism under event e

In summary, the algorithms described in this paper are all quite simple. This simplicity results from, and is an advantage of, our functional definition of the semantics of RSML. Unfortunately, the algorithms outlined above all have high worst-case complexity. For example, checking the union compositions is exponential with respect to the size of the guarding conditions, and checking determinism is O(n2) with respect to the number of parallel transitions. However, by using our functional composition approach, all algorithms work on fairly small problems, i.e., individual compositions, and this complexity is acceptable. The compositional approach allows us to determine if these properties are maintained when hierarchies, parallelism, and event propagation are introduced and avoids the problems of combinatorial explosion of the problem size and exponential growth in analysis effort. Experiments (described in the next section) have shown that our approach to analysis can be effectively applied to large systems.

5 Automated Analysis Tools and Their Evaluation of the TCAS II System Requirements Specification

Manually assuring d-completeness and consistency is an extremely tedious, time-consuming, and error-prone task. Tool support for the analysis algorithms have been implemented as an integral part of a simulator for RSML. The simulator accepts a textual representation of RSML and allows execution of a requirements specification.

A prototype graphical interface allows browsing the specification and animating executions. The analysis tools outlined in the previous section are integrated into this simulator. In addition to the results from the analysis algorithms (reporting inconsistency, incompleteness, and nondeterminism), the tools generate other useful information, such as uses hierarchies and event propagation tables.

Although the TCAS specification effort was originally planned to be experimental only, the government/industry groups responsible for TCAS II liked RSML so much that the specification was adopted as the official FAA TCAS II System Requirements Specification [18]. As a result, our initial baseline specification was subjected to an extensive (and expensive) independent verification and validation (IV&V) effort.

We have applied the analysis techniques described in this paper to major parts of our baseline TCAS II specification. Initial comparison of the errors found during IV&V and by our automated analysis indicates that inconsistency problems found during IV&V were also found by our automated analysis tools. Some subtle inconsistency problems not found during the official IV&V process were also found. More consistency problems are expected to be detected as the analysis progresses.

The analysis procedures also found many instances of incompleteness. Unfortunately, we have not been able to correlate these results with the IV&V effort since the IV&V effort did not include inspection for incompleteness. During IV&V, only the conditions under which state changes take place were reviewed; the conditions under which the state is not changed were not addressed.

The rest of this section provides some examples of the types of problems the analysis exposes. Drawbacks with the current implementation of the analysis procedures are also discussed.

5.1 D-completeness

Because d-completeness was not a priority in our initial TCAS requirements development (highest priority was placed on simply getting what was specified correct), we found abundant incompleteness during the later analysis process. In retrospect, we believe that if we had had our completeness analysis tools to alert us to incompleteness as we were developing the specification, the resulting document would have been much more complete. An example from the baseline document suffices to illustrate both the complexity of developing d-complete requirements and some problems with the current implementation of the analysis tools.

In TCAS, the concept of sensitivity level is used to determine how close an intruder is allowed to get before an advisory is presented to the pilot. A higher sensitivity level indicates a more sensitive setting of TCAS II, i.e., an advisory will be generated earlier (while the planes are farther apart). This example is taken from Auto-SL, a concept of sensitivity level based mainly on the aircraft altitude. Consider the transition in Figure 8. This transition defines when the model stays in Auto-SL state ASL-1. The automated analysis techniques detected an incompleteness|no transition out of the state is satisfied under a given condition (when a descend-inhibit-evaluated-event has occurred) shown in Figure 9. The analysis result reflects all conditions under which no transition out of this state can be taken. The abundance of predicates results from the diversity of the guarding conditions on the other transitions out of this state. This diversity makes it extremely difficult to determine manually (without the assistance of our analysis tools) the conditions for which no behavior has been specified.

Figure 8: The identity transition for Auto-SL state ASL-1

identity transition

Given the output shown in Figure 9, the analyst can determine what response the model should have for all conditions identified by the tool and modify the guarding conditions on the transitions to make the model d-complete (Figure 10). In this case the desired behavior was to stay in ASL-1 under all conditions identified by the analysis. In the general case, it is likely that more than one transition will need to be modified in order to cover these "forgotten" conditions. With this modification, the set of transitions out of state ASL-1 is d-complete , and the tool will report that there are no conditions where the behavior is unspecified (Figure 11).

No transition out of ASL_1
is satisfied under Descend_Inhibit_Evaluated_Event if :

Own_Air_Status == On_Ground               : F F F F F F F F F F F F F F F F F F F F F F 
Own_Air_Status == Airborne                : T T T T T T T T T T T T T T T T T T T T T T 
Traffic_Display_Permitted == cTrue        : F F F F F F F T T T T T T T T T T T F F F F 
Climb_Desc_Inhibit()                      : F F F F F F F F F F F F F F F F F F F F F F 
Radarout_EQ_0()                           : F T T T F F F F F T F F T T T F F F F F T F 
Radar_Bad_For_RADARLOST_Cycles()          : F . . . . . . T F . T F . . . . . . T F . T 
Effective_SL In One Of {ESL_1,ESL_2,ESL_3}: F F F F F F F F F F F F F F F F F F F F F F 
Effective_SL In State ESL_4               : T F F F F F F T T T T T F F F F F F T T T T 
Effective_SL In State ESL_5               : F T F F T F F F F F F F T F F T F F F F F F 
Effective_SL In State ESL_6               : F F T F F T F F F F F F F T F F T F F F F F 
Effective_SL In State ESL_7               : F F F T F F T F F F F F F F T F F T F F F F 
Own_Alt_Barometric >= ZSL4TO5             : . . . . . . . F . . F . . . . . . . F . . F 
Own_Alt_Barometric >= ZSL5TO6             : . F . . F . . . . . . . F . . F . . . . . . 
Own_Alt_Barometric >= ZSL6TO7             : . . F . . F . . . . . . . F . . F . . . . . 
Own_Alt_Barometric <= ZSL6TO5             : . . F . . F . . . . . . . F . . F . . . . . 
Own_Alt_Barometric <= ZSL7TO6             : . . . F . . F . . . . . . . F . . F . . . . 
Own_Alt_Radio <= ZSL4TO2                  : F . . . . . . T T F F F . . . . . . T T F F 
Own_Alt_Radio >= ZSL4TO5                  : . . . . . . . . . F . . . . . . . . . . F . 
Own_Alt_Radio > ZSL5TO4                   : . T . . . . . . . . . . T . . . . . . . . . 
Own_Alt_Radio <= ZSL5TO4                  : . F . . . . . . . . . . F . . . . . . . . .

Figure 9: D-completeness analysis result for Auto-SL state ASL-1

Figure 10: Transition modified for d-completeness
transition modified for d-completeness

No transition out of ASL_1
is satisfied under Descend_Inhibit_Evaluated_Event if :


Figure 11: Analysis result for the modified specification

5.1.1 Spurious Error Reports

During initial experiments with our first prototype tool, spurious error reports were not a serious problem [13]. All spurious reports could be traced either to (1) a lack of type checking capability or (2) the inability of the tool to adequately include information about the structure of the state machine in the analysis. For example, consider the input variable Air-Status of the enumerated type fAirborne, On-Groundg (appearing in the first two rows of Figure 9). Without information about the all inclusive and mutually exclusive nature of enumerated types, the tool would generate additional error reports and indicate that additional transitions out of ASL-1 are needed for the case

This is a clearly erroneous report because the input Air-Status must have one of these values; we do not need to specify what to do under this unsatisfiable condition. Similar problems relating to the structure of the state machine also led to spurious error reports. These drawbacks were trivial to address, and an updated version of the tool eliminates our previous problems with spurious errors.

Unfortunately, these changes do not eliminate all spurious error reports. Two features of the predicates in RSML complicates the analysis: (1) the use of simple arithmetic and (2) the use of mathematical functions. Contradictory predicates involving these features cannot be detected by the symbolic BDD approach. The number of spurious error reports increases dramatically when the number of predicates including these features increases. For example, the analysis tool may generate an error report including the condition in Table 6 (indicating that no transition has been specified for this condition). Any error report containing this condition is spurious because the predicates in Table 6 cannot be satisfied simultaneously. The current implementation of our tool is unable to eliminate this type of spurious error report. The problem is amplified when predicates use references to mathematical functions instead of constant values.

Table 6: A spurious report of an omitted condition.

spurious report

The problem with simple arithmetic expressions in the predicates can be addressed by using a theorem prover. Currently, however, the conflicts must be detected and eliminated by manual inspection. An ongoing project is attempting to augment our tool with theorem proving capability, and we hope to eliminate the problems with arithmetic expressions shortly.

The use of function references is a more serious challenge. We are investigating how assertions or invariants associated with the functions can be used to further increase accuracy. Unfortunately, completely eliminating spurious errors while still maintaining reasonable efficiency is an unrealistic goal. Thus, tool support to help the human analyst to interpret the analysis results and detect such problems manually is also being developed.

5.2 Consistency

A consistency problem exists when the guarding condition on more than one transition can be satisfied simultaneously.

The state machine modeling Effective-SL (which is related to Auto-SL) is shown in Figure 12. The bar on the side is a transition bus. Many state machines in the model were found to be fully interconnected, i.e., there are transitions between all the states in the machine; the transition bus was introduced to make the graphical representation cleaner.

Figure 12: Effective Sensitivity Level

An inconsistency can be detected between the transitions ESL-4->ESL-2 (Figure 5) and ESL-4->ESL-5 (Figure 13). The inconsistency (as reported from the analysis tool) can be seen in Figure 14: Column 3 of both transitions are satisfied by the condition. Since sensitivity level ESL-5 represents a sensitive setting and ESL-2 represents that advisories are shut off (no warnings are given to the pilot), a potentially hazardous inconsistency is present. After an evaluation of the inconsistency, it was determined that the guarding condition on the transition to ESL-2 was too weak and needed strengthening (Figure 15).

Figure 13: The transition from Effective-SL ESL-4 to ESL-5

ESL_4 --> ESL_2 conflicts with ESL_4 --> ESL_5 if

Auto_SL In State ASL_2                                : F
Auto_SL In One Of {ASL_2,ASL_4,ASL_5,ASL_6,ASL_7}     : T
Lowest_Ground() == 2                                  : T
Mode_Selector Equals One Of { TA_RA,TA_Only,3,4,5,6,7 } : T
Auto_SL In State ASL_5                                : T

Figure 14: Consistency analysis results for Effective-SL state ESL-4

Figure 15: The modified transition from Effective-SL ESL-4 to ESL-2

Unfortunately, correcting an inconsistency is often not as simple as strengthening the guarding condition on one of the transitions involved in the inconsistency. Inconsistencies sometimes arose from logical errors in the requirements and an extensive redesign of that part of the requirements document was needed.

Other approaches to requirements specification analysis are not concerned with this kind of inconsistency|it is simply viewed as nondeterminism and accepted as a part of the requirements. As was mentioned in Section 3, we view nondeterminism as an inconsistency that should, in most cases, be eliminated. At the least, each case needs to be carefully examined because nondeterminism can have a negative effect on safety (as shown by the example in this section).

6 Conclusions

This paper outlines a functional framework enabling compositional static analysis of statebased requirements and shows how the analysis for two fundamental qualities of requirements specifications -- d-completeness and consistency -- can be automated. The feasibility of the analysis has been demonstrated by analyzing major parts of a real life avionics system (TCAS II). The approach outlined in this paper has several advantages:

bulletThe analysis does not require generation of any part of the global reachability graph (either a complete representation or a symbolic representation)
bulletIt enables incremental analysis of the requirements. The pieces of the requirements document can be analyzed as they are being developed and the individual results combined at a later stage.
bulletIt helps identify the parts of the requirements needing re-analysis after changes to the document have been made.
bulletIt is a conservative approach, i.e., it is guaranteed that no d-incompleteness, inconsistency, or nondeterminism will go undetected.

We get these advantages by limiting the semantics of the specification language to those that can be described by functional composition. In doing this, we give up some freedom both in defining the semantics of the language and in the models that we allow users to build. We believe, however, that the increased power of the analysis that we can perform on complex models in comparison to other current approaches makes the tradeoff worthwhile. We found that eliminating the nondeterminism from the language made it easier for the TCAS reviewers to understand the model and find errors in it. So our restrictions have advantages in reviewability, correctness, and analysis, but they do cause some loss of flexibility in language design.

Because the BDDs we use to represent our AND/OR tables manipulate predicates symbolically, the analysis is conservative and may generate spurious error reports. The main source of spurious reports is the use of arithmetic and function references in the predicate definitions. Our tool is currently being refined to correct this problem. We are investigating the tradeoffs between efficiency and accuracy, and we are integrating the symbolic BDD approach with a theorem prover to achieve the level of accuracy required to easily interpret analysis results from the most complex parts of the TCAS requirements.

Our long term goal is to provide a suite of analysis tools to help find a wide variety of flaws in software requirements early during software development. Many desirable properties of requirements specification have been defined by Jaffe et al. [16], for example, non-reachability of hazardous states and path robustness properties. Additional properties are being defined for the human-computer interface (see Leveson [20] for some of the new criteria). Our goal is to formally define these properties in the RSML framework (and develop new ones suitable to this new framework) and provide efficient automated analysis procedures for these properties.


[1] J. Atlee and J. Gannon. State-based model checking of event-driven system requirements. In Proceedings of the ACM SIGSOFT '91 Conference on Software for Critical Systems. Software Engineering Notes. Volume 16 Number 5, 1991.

[2] G. R. Bruns, S. L. Gerhart, I. Forman, and M. Graf. Design technology assessment: The statecharts approach. Technical Report STP-107-86, MCC, March 1986.

[3] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986.

[4] J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill. Symbolic model chacking for sequential circuit verification. Technical Report CMU-CS-93-211, Carnegie Mellon University, July 1993.

[5] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, June 1990.

[6] E. M. Clarke, M. C. Browne, E. A. Emerson, and A. P. Sistla. Using temporal logic for automatic verification of finite state systems. In K.R. Apt, editor, Logics and Models of Concurrent Systems, pages 3-26. Springer-Verlag, Berlin, 1985.

[7] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic. ACM Transactions on Programming Languages and Systems, 8(2):244-263, April 1986.

[8] Patrice Godefroid, Gerhard J. Holzmann, and Dieder Pirottin. State space caching revisited. In Proceedings of the Fourth Workshop on Computer-Aided Verification, pages 175-186, 1992.

[9] D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231-274, 1987.

[10] D. Harel and A. Pnueli. On the development of reactive systems. In K.R. Apt, editor, Logics and Models of Concurrent Systems, pages 477-498. Springer-Verlag, 1985.

[11] D. Harel, A. Pnueli, J.P. Schmidt, and R. Sherman. On the formal semantics of statecharts (extended abstract). In 2nd Symposium on Logic in Computer Science, pages 54-64, Ithaca, NY, 1987.

[12] Mats P.E. Heimdahl. Static Analysis of State-Based Requirements: Analysis for Completeness and Consistency. PhD thesis, University of California, Irvine, 1994.

[13] Mats P.E. Heimdahl and Nancy G. Leveson. Completeness and Consistency Analysis of State-Based Requirements. In Proceedings of the 17th International Conference on Software Engineering, April 1995.

[14] Gerhard J. Holzmann. Tracing protocols. AT& T Technical Journal, 64(10), December 1985.

[15] Gerhard J. Holzmann. Automated protocol validation in Argos: Assertion proving and scatter searching. IEEE Transactions on Software Engineering, 13(6):683-696, June 1987.

[16] M. S. Jaffe, N. G. Leveson, M. P.E. Heimdahl, and B. Melhart. Software requirements analysis for real-time process-control systems. IEEE Transactions on Software Engineering, 17(3):241-258, March 1991.

[17] M.S. Jaffe. Completeness, Robustness, and Safety in Real-Time Software Requirements and Specifications. PhD thesis, University of California, Irvine, 1988.

[18] N. G. Leveson, M. Heimdahl, H. Hildreth, and J. Reese. TCAS II Requirements Specification.

[19] N. G. Leveson, M. P.E. Heimdahl, H. Hildreth, and J. D. Reese. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 20(9), September 1994.

[20] Nancy G. Leveson. Safeware: System Safety and Computers. Addison Wesley, 1995.

[21] R. Lutz. Targeting safety-related errors during software requirements analysis. In Proceedings of the First ACM SOGSOFT Symposium on the Foundations of Software Engineering, 1993.

[22] A. Pnueli and M. Shalev. What is in a step? In J. Klop, J. Meijer, and J. Rutten, editors, J.W. De Baker, Liber Amicorum, pages 373-400. CWI Amsterdam, 1989.

[23] A. P. Ravn and H. Richel. Requirements capture for embedded real-time systems. In IMACS Symposium MCTS, 1991.

[24] H. Richel and A. P. Ravn. Requirements capture for computer based systems. Technical Report ID/DTH HR 2/2, Technical University of Denmark, October 1990.

[25] J. Rushby and F. von Henke. Formal verification of algorithms for critical systems. IEEE Transactions on Software Engineering, 19(1):13-23, January 1993.

A Auxiliary Definitions

The definitions in this appendix describe the hierarchical and parallel structure of the state machine used in both RSML and Statecharts. The definitions are adopted from [11, 22].

Definition 12 The least common parent (lcp) of the states in the set X2S, lcp(X) = y, is defined as:

Informally, X has to be a subset of the descendants of lcp(X) and σ*(lcp(X)) has to be the smallest set containing both X and lcp(X) where lcp(X) is the smallest superstate containing all states in X.

The graphical notation used in Statecharts and RSML requires that the hierarchy of states must be organized in a tree structure.

Definition 13 There must exist a state x ∈ S, known as the root, satisfying:

For example, in Figure 6 lcp({G, H}) = E, lcp({B, I}) = A, and the root is A.

The partitioning function π divides the descendants of any given state into parallel components. If two descendants of a state are members of different parallel components, they are said to be in parallel.

Definition 14 States x and y are parallel (x ⊥ y) iff:

Informally, the states x and y are parallel iff they are (or are contained under) states from different parallel components of their least common parent. In Figure 6, for example, H and B, B and D, and F and H are all pairwise parallel. Examples of non-parallel states include (1) B and C and (2) D and H.

Definition 15 A set X2S is said to be parallel iff:

That is, all elements of X are pairwise parallel. The set {B, G, I} is an example of a parallel set.

Definition 16 A set X2P is consistent iff:

Informally, a set of states x is consistent iff all states in X are either ancestrally related or parallel. As an example, for the states in Figure 6, the sets {F, H} and {E, H} are both consistent, but {D, H} is not.

Definition 17 A set X2S is said to be maximally consistent iff:

The concept of maximally consistent is best explained with an example. Consider Figure 6 and assume the machine is in state H. Given the structure of the state hierarchy, it is clear that if you are in H, you also are in E and A. The concept of maximally consistent "fills in the blanks" in a consistent set: If you are in H, you also have to be in Ef and A. A maximally consistent set of states is known as a configuration of M . The set {A, B, E, F, H} is maximally consistent. This set defines one possible configuration of M.

We can now formally define the set of global states of M:

Definition 18 The set of global states C is defined as:

This concludes the formal definition of the structure of the states making up the graphical notation used in RSML (and Statecharts). Note again that these definitions are essentially identical to the definition of the hierarchical structure of Statecharts [11, 22].

Home Products Services Publications White Papers About Us

Copyright 2003 Safeware Engineering Corporation. All rights reserved