%0 Conference Proceedings
%T Synchronous Interface Theories and Time Triggered Scheduling
%+ AELOS
%+ Efficient STAtistical methods in SYstems of systems (ESTASYS)
%+ Institute of Science and Technology [Klosterneuburg, Austria] (IST Austria)
%A Delahaye, Benot
%A Fahrenberg, Uli
%A Legay, Axel
%A Ničković, Dejan
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE)
%C Stockholm, Sweden
%Y Holger Giese
%Y Grigore Rosu
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-7273
%P 203-218
%8 2012-06-13
%D 2012
%R 10.1007/978-3-642-30793-5_13
%Z Computer Science [cs]Conference papers
%X We propose synchronous interfaces, a new interface theory for discrete-time systems. We use an application to time-triggered scheduling to drive the design choices for our formalism; in particular, additionally to deriving useful mathematical properties, we focus on providing 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 theories and real-time scheduling, where we demonstrate a fully automatic framework for the incremental computation of time-triggered schedules.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01087992/document
%2 https://inria.hal.science/hal-01087992/file/forte.pdf
%L hal-01087992
%U https://inria.hal.science/hal-01087992
%~ UNIV-NANTES
%~ INSTITUT-TELECOM
%~ EC-PARIS
%~ UNIV-RENNES1
%~ CNRS
%~ INRIA
%~ UNIV-UBS
%~ INSA-RENNES
%~ INRIA-RENNES
%~ IRISA
%~ LINA
%~ IRISA_SET
%~ INRIA_TEST
%~ LINA-AELOS
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ IRISA-D4
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ UR1-HAL
%~ UR1-MATH-STIC
%~ IFIP-FORTE
%~ LS2N
%~ UR1-UFR-ISTIC
%~ IFIP-FMOODS
%~ IFIP-LNCS-7273
%~ IFIP-2010
%~ TEST-UNIV-RENNES
%~ TEST-UR-CSS
%~ UNIV-RENNES
%~ INRIA-RENGRE
%~ INSTITUTS-TELECOM
%~ UR1-MATH-NUM
%~ NANTES-UNIVERSITE
%~ UNIV-NANTES-AV2022