Relating Real-Time System Contracts with Software Function Contracts

Assume-guarantee contracts have previously been shown to be an effective means for the formal specification and verification of systems and software in a scalable, modular fashion. However, there remain challenges in bridging system-level contracts with software-level contracts, and more specifically, in relating system-level, trace-based execution semantics to software-level, pre/post-state based ones. In this paper, we first provide a general description of how an automotive system can look, and then use the OCRA framework to model a concrete industrial system with periodically scheduled, terminating C functions. We show how the software-level contracts, expressed in the specification language ACSL, can be formally related to the system-level contracts, expressed in the temporal logic MITL, using a super-dense semantics, by formalising scheduling assumptions and translating the ACSL contracts into MITL. Finally, we discuss additional challenges in specifying a more realistic version of the system.