SCAA colloquium: Brayan Shali

Title: A contract theory for linear systems

 

Abstract: We introduce contracts for linear time-invariant systems with inputs and outputs. Contracts are used to express formal specifications on the dynamic behaviour of such systems through two aspects: assumptions and guarantees. The assumptions capture the available knowledge about the dynamic behaviour of the environment in which the system is supposed to operate. The guarantees capture the required dynamic behaviour of the system when interconnected with its environment. We also define and characterize notions of contract refinement and contract conjunction. The former allows one to compare contracts and the latter allows one to fuse the specifications expressed by multiple contracts. Finally, we also define and characterize notions of contract composition, which can be used to analyse and design interconnections of systems.