AOCS Modeling by Åbo Akademi. This section presents some technical details of the attempted formal development of an AOCS model at Åbo Akademi. The Event-B project Modes_v2 [RD10], the current model, consists of the initial abstract specification and its two refinements. The model is “monolithic” though the events belonging to different managers can be easily identified. In future refinement steps, decomposition of the system (according to Figure 9) is planned, explicitly introducing communication mechanisms between components in the form of procedure calls and monitored variables. The operations in the machine abstractly describe the default scenario in which the system tries to achieve the top (most operational) global mode. The default mode scenario can be interrupted by the FDIR Manager, which non-deterministically issues mode transition requests, backtracking the system to the current or one of more degraded modes. The actual error handling and resolution is abstracted away until the second refinement step. The proved invariant properties relate the ordering of global modes with the current mode transition. For example, the fact that the current mode transition is FDIR-initiated is logically equivalent to the one that the target mode is less or equal (according to the global mode ordering) to the current mode. Similarly as global modes, unit configurations are introduced as a total order. However, as been pointed out during discussions with SSF, a total order is a too strict requirement for unit configurations, while a partial order is a much more realistic assumption for this kind of systems. The necessary modifications will be done for the next version of models. The relationship between global modes and the required unit configurations is introduced in the form of an abstract data structure (Mode_configs) in the accompanying context. The essential properties of Mode_configs are formulated as axioms. Mode_configs can be considered as a system parameter that should be supplied (instantiated) at some point of the system development. One of the most essential properties is order preservation between global modes and unit configurations. In other words, it means that “increasing” (i.e., moving to a more operational) the current global mode corresponds to “increasing” or at least leaving the same unit configurations. There are a few rare exceptions when this property does not hold in the AOCS system. However, while taking these exceptions into account, this property can be considered...
