Comparison between SSF’s and Åbo Akademi’s AOCS Modeling Approaches. SSF’s AOCS model development stems from the detailed description of the AOCS system provided as Ada code. Its goal is to produce Event-B models as close as possible to the provided Ada description, reflecting both its overall complexity and organizational structure. As a result, the developed models put the Rodin Platform to a serious test by sheer number of variables and events needed to represent the level of detail present in the Ada description, which is a still somewhat simplified version of the real AOCS subsystem. It also highlights the lack of Rodin Platform features that are sorely needed to improve its scalability such as decomposition and modularization support, modeling of procedure calls, control flow management etc. To faithfully reflect the control flow and organizational structure of the Ada description, many special variables (e.g., program counters or the variables to model formal parameters of called procedures) have to be introduced. This makes difficult to formulate more general properties of the system, for example, that some property which is true at certain point of execution is still true after a number of steps down the road of the modeled control flow. The formal development attempted by Åbo follows the standard techniques of top-down modeling by refinement. The provided Ada document is used more like a reference point or general requirements document. The goal of the development is to identify generic specification and refinement steps or patterns as well as general properties that are typical for this class of systems. The development starts with a much simplified architecture of the AOCS system, which is then unfolded layer by layer by refinement. At the same time, the selected general properties about mode management are formulated and proved. This is possible because the level of complexity represented in models is still manageable. The current development is still very incomplete. The refinement process will be continued, thus slowly approaching the level of detail that is already covered by SSF models. To avoid explosion of complexity, the use of newly developed decomposition and modularization techniques [RD7], [RD8] (e.g., the modularization plug-in) will be investigated.
