Home > Publications > Completeness and Consistency |

## Completeness and Consistency in Hierarchical State-Based Requirements |

Mats P.E. Heimdahl
Nancy G. Leveson University of Washington Computer Science and Engineering, FR-35 Seattle, WA 98195 ## AbstractThis 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 IntroductionA 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 - Every state must have a behavior (transition) defined for every possible input.
- The logical or of the conditions on every transition out of any state must form a tautology.
- 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 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.
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 NotationRSML 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.
Transitions are taken upon the occurrence of the 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 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). 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 FrameworkThe 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
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 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 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-MachinesAn RSML state machine M can be described by a six-tuple: where:
σ is a function mapping a state onto a set of states ( Definition 1 The hierarchy function σ is defined by:
σ π 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 (π
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).
F is also referred to as the
behavior of M.In the definitions above, there are few restrictions on the nature of a
The remainder of this section is devoted to the next-state relation ## 3.2 Next-State MappingThe 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 In the graphical notation, these simple functions are defined by
transitions. The
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
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 composition is allowed if both possible serial compositions
are allowed. If In RSML, union composition occurs between nonparallel transitions
triggered by the same event. For example, the functions representing the
transitions Transitions triggered by the same event, but in parallel state
components, are composed in parallel. In Figure 7, transitions Finally, serial application is caused by the event propagation
mechanism. Assume the transition 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 Q are sets of
states, _{d}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 Q
and the set that is entered by _{s}Q. In the definition
above, the set { _{d}c | (x ∈ c)
∧ p(c) } defines the domain of the
function (Dom(f)), and Q and _{s}Q
are the _{d}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.
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 g
intrfoduced in the parallel state component π_{i}. In Figure
7, the function represented by t to π_{4} belongs_{1}(A).
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,...., σ(s)
is partitioned. In Figure 7, for example, σ(A) is partitioned into
four parallel state components.
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 The set of all functions with the output action e is
denoted F. The function defining the behavior of ^{e}M
under the event e must be applied after a function with the
action e has been applied, i.e., ... F.
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.^{e}(ƒ_{e}(...))...
An evaluation of
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 ApproachIf the relation 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.
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. ```
```
```
```
Table 1: Data structures used to represent the state space ```
```
```
```
Table 2: Data structure for conflicting 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
e as an action, i.e., if _{2}e
occurs, the transition is taken and _{1}e is generated.
The event _{2}e 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._{2}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.
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 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].```
```
```
```
Table 4: Data structure for non-deterministic pairs of transition ```
```
```
```
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 ## 5 Automated Analysis Tools and Their Evaluation of the TCAS II System Requirements SpecificationManually 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-completenessBecause 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. 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). ```
```
```
```
Figure 9: D-completeness analysis result for Auto-SL state ASL-1
Figure 11: Analysis result for the modified specification ## 5.1.1 Spurious Error ReportsDuring 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. 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 ConsistencyA 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. 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 14: Consistency analysis results for Effective-SL state ESL-4 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 ConclusionsThis 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:
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 ## References[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 DefinitionsThe 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].
Informally, 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.
For example, in Figure 6 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.
Informally, the states
That is, all elements of
consistent iff:Informally, a set of states
maximally consistent iff:The concept of maximally consistent is best explained with an example.
Consider Figure 6 and assume the machine is in state We can now formally define the set of
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]. |

Copyright © 2003 Safeware Engineering Corporation. All rights reserved