Next: 1 Background Up: FoCBS
K. Lano, J. Bicarregui, T. Maibaum
Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ
Dept. of Informatics, University of Lisbon, Campo Grande, 1700 Lisbon
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.