A next step addresses behaviour that does obviously not contribute to the requirement. For example, most behaviour for system shutdown has been removed as we consider the system to be reactive and non-terminating. Thereby a number of events for system shutdown became obsolete. Similarly, the channels and their voting and monitoring can be removed from the model since they don't affect the studied requirement. This leads to both a leaner structure and behaviour. Furthermore, some behaviour can be encoded more eficiently. For example, the state-machine of class SysModel has been modified to react directly on events of the new type evTick modelling passing time. evTick events are declared to be sent by the environment at any point in time.
In other words, the model checker is able to notify the SysModel any time about passed time, thereby abstracting from the particular timing in the executable model. Since we use a configuration without non-voted sensors, the objects of class SysRun can be removed if the actions that trigger the computation of the arithmetic average is moved to SysModel.
Evidently all these steps are not suficient to treat the major cause for complexity in the example, namely the sheer amount of objects and links. Therefore the model has been focused to the object diagram shown in Fig. "Object diagram". As the requirement applies to all flight control computers and all kinds of aircraft parameters independently, it is by symmetry1 suficient to consider only one flight control computer and within this one only a single kind of value, and thus a single set of sensors and voting and monitoring objects. The remaining flight control computers are not necessary to trigger their sensors, since sensor values are obtained as inputs, i.e. at the point in time when they are read. This has, in addition to a smaller number of objects whose attributes need not be represented, the effect that links can be encoded using types with smaller domains. Fewer objects simply need a smaller domain of identities.
Figure 1: Formalisation of the requirement as introduced in unit Formal Verification of the Sensor Voting UML Model. It directly corresponds to a C++ expression that is used to instantiate the corresponding pattern from the OFFIS pattern library (cf. The UML Verification Environment I). Note that it is a state invariant, that is, an invariant that doesn't employ temporal modalities. p System denotes a top-level object of the model that is not part of any other object. In UVE expressions, top-level objects can be navigated from a (virtual) root object
denoted by ‘root’.
The remaining major cause for complexity is the large number of active objects, i.e. the concurrency in the model. Recall that both classes RTC and SysRun have been removed from the model. So SysModel remains as the only active class in addition to the global thread all other objects run in. As the actions of SysModel are synchronised with the rest of the model, it need not remain active. The model with active SysModel is equivalent to a single thread model.
Finally we obtained a model structured similar to the one shown in Treating Complexity by Abstraction I with about 16 objects, 8 of them with state-machine, and only 4 kinds of events all running in a single thread.