Behavioural assume-guarantee contracts for linear dynamical systems

Motivated by the growing requirements on theoperation of complex engineering systems, we present con-tracts as specifications for continuous-time linear dynamicalsystems with inputs and outputs. A contract is defined asa pair of assumptions and guarantees, both characterized ina behavioural framework. The assumptions encapsulate theavailable information about the dynamic behaviour of theenvironment in which the system is supposed to operate, whilethe guarantees express the desired dynamic behaviour of thesystem when interconnected with relevant environments. Inaddition to defining contracts, we characterize contract imple-mentation, and we find necessary conditions for the existence ofan implementation. We also characterize contract refinement,which is used to characterize contract conjunction in two specialcases. These concepts are then illustrated by an example of avehicle following system