The theoretical foundation presented in this paper significantly enables the application of formal methods in software engineering. The paper mentions avionics software as an example of a reactive system that motivates research on the semantics of behavioral hierarchy, and Ruleset Markup Language (RSML) as one formalism to describe it. Therefore, this review uses the context of real-time embedded systems controlling physical processes (such as vehicles moving in space) to discuss this paper.

The paper provides certain semantics for behavioral hierarchy in state machine models and specifications. Its target audience seems to be the formal methods research community.

Although behavioral hierarchies are used in several state machine modeling tools, and the unified modeling language (UML) standard, their respective semantics do not allow exploitation of their hierarchical structure for efficient formal analysis. This paper defines certain semantic rules on the behavioral hierarchy that allow application of formal verification methods more efficiently. Behavior models that follow these semantic rules (or constraints) will be easier to transform into correct implementations. It will also be easier to transform these models from one tool environment to another tool environment.

The defined semantic rules are analogous to those found in well-structured object-oriented programming languages, namely, variable scoping, encapsulation, abstraction, and order of control flow in the behavioral hierarchy. These rules are intended to support correct composition of complex units from simpler units. Restrictions on transitions across levels to entry and exit points, and variable-hiding rules, support abstraction and encapsulation up the composition hierarchy. Conversely, refinement relations support design-elaboration and implementation in a manner that enables verification against specifications. Mode instantiation rules support reuse.

In the tradition of many other papers in this field, the term “semantics” is used here in the context of some assumed background knowledge. The paper uses the term “denotational semantics,” leading one to expect a semantics definition that is explicit and self-sufficient; it should not require any implicit knowledge, although underlying semantics definitions may be incorporated by reference. Semantic definitions should be interpretable by machines, as well as by humans. In this paper, however, it was difficult to understand the semantics, perhaps due to its assumed context. Some of these difficulties are discussed below.

The paper builds on an earlier definition of the compositional language of a “reactive module,” in which the atomic module is a state machine. It mentions input variables, output variables, and states, yet one cannot trace the references back to fundamentals, such as the definition of a state, a finite state machine, or a Mealy machine.

A distinguishing characteristic of physical processes, such as vehicle motion, is that a state change takes time. However, it is not clear how the semantics here accommodates the elapsed time. There seems to be an assumption of transition in zero time. This leaves unanswered questions about the semantics of a discrete state, and the constraints under which the discretization of the state space is valid.

When discussing semantic equivalence, the paper contrasts its approach of “observational equivalence” against the commonly used structural isomorphism of a state-transition graph. However, it is not clear how the context of two “observationally equivalent” terms is defined to be the same, independent of some notion of a system state space.

The paper uses the terms “step,” “round,” and “transition,” but their distinction or relationship is unclear. It talks about an update round, an update action, an update relation, and an update rule, and about “guarded commands,” but it does not define these terms explicitly, nor does it cite underlying references (for example, Dijsktra’s work [1]).

The paper does not introduce the notion of an event, nor does it discuss its omission. It is not clear whether this is a religious divide between the state-oriented theorists and the event-oriented theorists. It seems that a semantic framework that clearly describes the relationship among states, events, and actions would be easier to understand, and better suited to modeling the real world of physical processes.

Although the theory presented here may be valid for various complex types of interactions, use of a domain with simpler interactions (for example, a closed system to control physical processes, such as motion) would simplify explanation. It would be valuable to devise the formalism to specify the constraints on the environment (the closed system) and constraints on the interactions.