Composition of Reactive System Components

K. Lano, J. Bicarregui, T. Maibaum
Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ
kcl@doc.ic.ac.uk -
J. Fiadeiro
Dept. of Informatics, University of Lisbon, Campo Grande, 1700 Lisbon

Abstract:

This paper will present the case for using a formal component-based specification technique for reactive systems, such as the Object Calculus of Fiadeiro and Maibaum. The Object Calculus provides a modular, highly declarative and abstract specification language, suitable for refinement using model-based design notations such as B or VDM.

In the Object Calculus, pre/post style specifications of the effect of actions can be given, together with temporal logic specifications of expected histories of behaviour of the system.

Keywords: Temporal logic, Reactive systems, Program specification, Object Calculus, Specification languages.

Workshop Goals: Investigate application of formal specification in component-based systems, particularly reactive systems.