Figure 3 – SpecTRM-RL Output Specification

 

 

The next set of attributes relates to the capacity of the environment around the software for handling output messages.  Outputs must not be sent frequently enough to overwhelm the load tolerance of the environment.  SpecTRM-RL outputs describe their load, minimum time between outputs, and maximum time between outputs.  Output load problems have contributed to accidents.  At one point during the Three Mile Island accident, a printer that reported problems fell two hours behind the state of the system (ref. 4).  In the case of the command shown in figure 3, the load entry reads that the software is required not to send output commands while the robot is considered to be in motion — the physical characteristics of motion should prevent the output command from exceeding the load acceptable to the motion controller.  To a reviewer of the specification, this may immediately raise questions as to whether the software could enter a state where the controller inferred that the robot was still while it was actually moving.  Another question would be whether the motor controller’s message load might be exceeded in the period of time between the issuance of a movement command and the receipt of feedback indicating that the robot began movement.  These are exactly the kinds of questions that the completeness criteria are designed to provoke, and SpecTRM-RL facilitates uncovering both these questions and their answers.

Feedback loops must be included in the software specification.  Accidents occur when the system state inferred by the software controller does not match the actual state of the system.  If no feedback is provided, the controller software cannot determine whether the system has changed based on the commands it has sent.  This can lead to dangerous system behavior.  For example, feedback from the “Move Relative” command is provided by position readings after each move.  Because physical motion is imprecise, if position feedback were not provided, a steadily degrading consistency between the controller’s coordinates for the robot and the robot’s actual position might result in the robot being commanded into a solid object.  Feedback information also addresses latency.  If feedback inputs arrive before the latency period for a command has elapsed, it is possible that the input is spurious.

Another completeness criterion suggests that all outputs must be reversible.  With rare exception, any command that can be given to a system by a software controller should be reversible.  The output specification format of SpecTRM-RL includes an attribute for describing what output reverses the action taken.  The description of “Move Relative” (figure 3) shows that the “Stop” command can be used to stop motion.  Using the triggering condition tables and working backward into the model, it is also possible to use these outputs to verify another of the criteria: if one output is to reverse another, there must be a path through the state space between them.

The triggering condition AND/OR table is a useful tool itself for applying completeness criteria.  The criteria assert that reachable hazardous states should be eliminated whenever possible.  When they cannot be eliminated, their frequency and duration should be reduced as much as possible.  The triggering condition is a guard condition on the production of the output.  Because of SpecTRM-RL’s readable syntax, these guard conditions can be reviewed by domain experts to ensure that an output cannot be produced under circumstances that make the output behavior hazardous.

Modes:  Modes represent a collection of system behaviors.   For example, if the industrial robot is in operator control mode, it will behave differently than when it is in computer control mode.  Mode behavior, particularly regarding mode transitions and mode confusion, has contributed to a number of accidents.  SpecTRM-RL specifies modes as shown in figure 4.

 

 

 

 

Figure 4 – SpecTRM-RL Mode Specification

There are fewer attributes at the beginning of mode specifications than there are for outputs.  The references attribute is filled in with a list of all the elements of the model that are used in the definition of the control mode.  While manual maintenance of these lists might grow tedious, they can be automatically generated by tools.  The model element names listed in the references section can be turned into hyperlinks by most editors, allowing easy navigation around the model.  By providing an easy navigation path through related model elements, the references list can aid in checking any of the completeness criteria that involve multiple model elements.  For example, one criterion states that all information from sensors should be used in the SpecTRM-RL model.  An unused input suggests some incompleteness in the requirements for the software.  Automated tools can verify that every input appears in at least one model element’s references attribute.

Modes also have a list of the elements in which they appear.  This attribute can be used to navigate through the SpecTRM-RL model looking for system behaviors that are affected by the mode.  One of the completeness criteria is that states and modes should not inhibit the production of later required outputs.  For example, if the robot is in computer-controlled mode, it is conceivable that the operator may wish to have the robot take a different path.  Examining the list of model elements in the appears in attribute, it becomes apparent that the robot cannot follow operator movement commands unless the movement control mode can be changed to operator control.  Examining that transition, it becomes evident that any time the deadman switch is released, the system returns to operator control.  Thus, in this example and for this case, the criterion is satisfied.

Lastly, the mode specification includes a definition of possible mode values and the conditions under which the mode changes.  Figure 4 shows four example modes: startup, operator, computer, and halted.  Each of these modes is associated with an AND/OR table.  These AND/OR tables follow the same rules as those for output triggering conditions.  If every row in a T/F/* column matches against the expressions in the first column, that column is true.  If any column in a table is true, the entire table is true.  If an AND/OR table is true, the mode is changed to the mode attached to that table.

These AND/OR transition tables are suitable for checking a variety of completeness criteria.  One criterion checks that the software must always start up in a safe configuration.  The use of a startup mode to handle the initialization of the software provides an opportunity to ensure that the software’s model of the controlled plant can be correctly initialized.  Another criterion is that paths to modes that increase the hazard of the system should be easy to abort, whereas paths that reduce the hazard of the system should be plentiful and easy to follow.  In figure 4, many conditions are sufficient to bring the industrial robot under operator control, but there is only one way to put the robot under computer control.

States:  State elements in SpecTRM-RL represent the model that the software controller has of the system being controlled.  Inputs to the software change the inferred system state, which may in turn change the mode of the system or trigger outputs.  An example SpecTRM-RL state specification from the industrial robot example is included in figure 5.  The references and appears in attributes in the state definition are analogous to those discussed above for modes.  The same associated criteria can be checked for states.

 

Figure 5 – SpecTRM-RL State Specification

SpecTRM-RL state specifications model the state of the process.  If no new information is received from the modeled process for some time, it is unsafe to rely on the outdated information.  For example, when the robot switches from computer control to operator control (figure 4), commands sent to the motor controller are velocity based rather than position based.  In order to operate correctly and safely, the robot’s motor controller must be set to relative position mode or velocity mode accordingly.  If MAPS has not received an input from the motor controller in some time, it cannot be sure what mode the motor controller is really in — particularly if some suspension of input processing may have taken place.  Unknown gives the engineer writing the requirements a way to reason about situations in which the controller does not have information. 

The AND/OR transition tables are, in other respects, similar to the mode transition tables discussed above.  A state element transitions to a new state value when the AND/OR table associated with that value is true.  The tables themselves are easy to read and review.  Two completeness criteria, the robustness and nondeterminism criteria, are easy to check with automated tools once the specification is written in SpecTRM-RL.  To meet the robustness criteria, there must be no conditions under which all the AND/OR tables are false.  For example, in figure 5, suppose that Power Up is false and the “Motor Controller Setting” input is not obsolete, uninitialized, relative, or velocity.  Under those conditions, no table is true, and the state machine cannot make a transition of any kind.  In reality, the only values possible for the input are the four tested in the AND/OR tables, so the state description is robust.  Software-related accidents are often caused by unhandled cases in requirements specifications.  Robustness ensures that all cases are handled by the state element.

The nondeterminism criterion states that all SpecTRM-RL state elements must be deterministic in their behavior.  To be deterministic, there must not be any circumstances under which more than one AND/OR table can be true at the same time.  The state element described in figure 5 is not deterministic. Suppose that power up is true, meaning that the software has just been started, and a motor controller setting input comes in with a value of relative at the same time.  Both the unknown AND/OR table and the relative AND/OR table are true.  In practice, the behavior of the software will be implementation dependent.  It is very difficult to analyze nondeterministic systems for properties such as safety.  Therefore, it is strongly desirable to remove nondeterminism from a system.  Automated tools can help enforce both robustness and determinism in a SpecTRM-RL specification.

Inputs:  Inputs are the last major grouping of specification elements in SpecTRM-RL.  An example input from the industrial robot example is shown in figure 6.  The general form of the input is very similar to the other SpecTRM-RL model elements.  First, a series of attributes describes the input.  Second, a series of tables defines the behavior of the input.