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, c₀ ∈ (2^S × 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 C ↣ I, where C ⊆ (2^S &#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 c_i 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: ƒ _t6 ∘ ƒ_t5(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 Q_s and Q_d 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 Q_s and the set that is entered by Q_d. In the definition above, the set &#x007B c | (x &#x2208 c) &#x2227 p(c) &#x007D defines the domain of the function (Dom(f)), and Q_s and Q_d 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) = ∅:

g_a = ∅

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 ⊐ C0;_i denotes a function (transition) g intrfoduced in the parallel state component π_i. In Figure 7, the function represented by t₄ belongs to π₁(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,....,k_s} 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 F^e. 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., ... F^e(ƒ_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.

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 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 e₁ may generate event e₂ as an action, i.e., if e₁ occurs, the transition is taken and e₂ is generated. The event 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.

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(n²) 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].

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 O(n²) 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.

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 10: Transition modified for d-completeness

No transition out of ASL_1
is satisfied under Descend_Inhibit_Evaluated_Event if :

FALSE

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.

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:

	The analysis does not require generation of any part of the global reachability graph (either a complete representation or a symbolic representation)
	It 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.
	It helps identify the parts of the requirements needing re-analysis after changes to the document have been made.
	It 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.

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 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 X ∈ 2^S, 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 X ∈ 2^S 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 X ∈ 2^P 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 X ∈ 2^S 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].