Functional specification and proof of correctness for time dependent behaviour of reactive systems

Abstract

Abstract A functional formalism for describing and reasoning about the time dependent behaviour of reactive systems is presented. The model is event based and can describe the histories of events with finite duration. It is a generalisation of the model of Caspi and Halbwachs (1986). A set of tools with their operations are introduced in the formalism and structure theorems characterising the algebra of events are proved. The power of this extended model is illustrated through the formal specification and correctness proof for a problem chosen from robotics.