Synchronous Interface Theories and Time Triggered Scheduling

Abstract. We propose synchronous interfaces, a new interface theory for discrete-time systems. We use an application to time-triggered schedul-ing to drive the design choices for our formalism; in particular, addi-tionally to deriving useful mathematical properties, we focus on provid-ing a syntax which is adapted to natural high-level system modeling. As a result, we develop an interface model that relies on a guarded-command based language and is equipped with shared variables and explicit discrete-time clocks. We define all standard interface operations: compatibility checking, composition, refinement, and shared refinement. Apart from the synchronous interface model, the contribution of this paper is the establishment of a formal relation between interface theo-ries and real-time scheduling, where we demonstrate a fully automatic framework for the incremental computation of time-triggered schedules.