Next: References
Up: Composition of Reactive System
Previous: 2.2 Design and Implementation
We have shown that the Object Calculus can be used to provide a highly abstract and declarative specification of the behaviour of the steam boiler. We have formalised most aspects of the system. An executable controller has been produced and tested against the FZI simulator. Approximately 1 person week was used in writing the abstract specification, and 2 person weeks in developing the B design and implementation, including verification activities. B has been shown to be effective for industrial specification and to be comprehensible by `average programmers'. We believe that the Object Calculus is also quite easy to relate to reactive system concepts and to notations such as statecharts, which it generalises. The papers [4,5] describe how statecharts can be mapped to the Object Calculus.
Some specifications of [2] address issues which we do not consider, such as the calculation of optimal control points or the probabilistic behaviour of device failures. Our abstract specification adopts the approach of [7] in working at the macro step level in order to simplify the description. The B design is at the micro step level. The Object Calculus description is also related to the rule-based approaches used in [3] and [9], and suffers a similar problem of consistency obligations between rules. Our controller design model, like that of [6], adopts a purely reactive system approach, whereby events are assumed to happen one at a time and are reacted to in the order of their arrival. An alternative structuring approach would be to use a time-based partitioning of modules, whereby the actions relevant to the initialisation phase of the steam boiler operation are placed in a theory separate from the actions and attributes of the running phase.
The mapping from Object Calculus to B is systematic (theories correspond to machines) but is not entirely automatic, since a design process is involved. Future work will classify different design choices for this translation, and relate B structuring formally to the Object Calculus. The Object Calculus has also been related to the UNITY approach for reactive system specification [12].
Other research directions include real-time extensions and durative actions, and deontic logic in order to handle failure states more naturally.
K. Lano, J. Bicarregui, T. Maibaum, and J. Fiadeiro