---
_id: '4631'
abstract:
- lang: eng
  text: We present a theory of timed interfaces, which is capable of specifying both
    the timing of the inputs a component expects from the environment, and the timing
    of the outputs it can produce. Two timed interfaces are compatible if there is
    a way to use them together such that their timing expectations are met. Our theory
    provides algorithms for checking the compatibility between two interfaces and
    for deriving the composite interface; the theory can thus be viewed as a type
    system for real-time interaction. Technically, a timed interface is encoded as
    a timed game between two players, representing the inputs and outputs of the component.
    The algorithms for compatibility checking and interface composition are thus derived
    from algorithms for solving timed games.
acknowledgement: This research was supported in part by the NSF CAREER award CCR-0132780,
  the NSF grant CCR-9988172 the AFOSR MURI grant F49620-00-1-0327, the DARPA PCES
  grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, and the ONR grant N00014-02-1-0671.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Mariëlle
  full_name: Stoelinga, Mariëlle
  last_name: Stoelinga
citation:
  ama: 'De Alfaro L, Henzinger TA, Stoelinga M. Timed interfaces. In: <i>Proceedings
    of the 2nd International Conference on Embedded Software</i>. Vol 2491. ACM; 2002:108-122.
    doi:<a href="https://doi.org/10.1007/3-540-45828-X_9">10.1007/3-540-45828-X_9</a>'
  apa: 'De Alfaro, L., Henzinger, T. A., &#38; Stoelinga, M. (2002). Timed interfaces.
    In <i>Proceedings of the 2nd International Conference on Embedded Software</i>
    (Vol. 2491, pp. 108–122). Grenoble, France: ACM. <a href="https://doi.org/10.1007/3-540-45828-X_9">https://doi.org/10.1007/3-540-45828-X_9</a>'
  chicago: De Alfaro, Luca, Thomas A Henzinger, and Mariëlle Stoelinga. “Timed Interfaces.”
    In <i>Proceedings of the 2nd International Conference on Embedded Software</i>,
    2491:108–22. ACM, 2002. <a href="https://doi.org/10.1007/3-540-45828-X_9">https://doi.org/10.1007/3-540-45828-X_9</a>.
  ieee: L. De Alfaro, T. A. Henzinger, and M. Stoelinga, “Timed interfaces,” in <i>Proceedings
    of the 2nd International Conference on Embedded Software</i>, Grenoble, France,
    2002, vol. 2491, pp. 108–122.
  ista: 'De Alfaro L, Henzinger TA, Stoelinga M. 2002. Timed interfaces. Proceedings
    of the 2nd International Conference on Embedded Software. EMSOFT: Embedded Software
    , LNCS, vol. 2491, 108–122.'
  mla: De Alfaro, Luca, et al. “Timed Interfaces.” <i>Proceedings of the 2nd International
    Conference on Embedded Software</i>, vol. 2491, ACM, 2002, pp. 108–22, doi:<a
    href="https://doi.org/10.1007/3-540-45828-X_9">10.1007/3-540-45828-X_9</a>.
  short: L. De Alfaro, T.A. Henzinger, M. Stoelinga, in:, Proceedings of the 2nd International
    Conference on Embedded Software, ACM, 2002, pp. 108–122.
conference:
  end_date: 2002-10-09
  location: Grenoble, France
  name: 'EMSOFT: Embedded Software '
  start_date: 2002-10-07
date_created: 2018-12-11T12:09:51Z
date_published: 2002-10-24T00:00:00Z
date_updated: 2023-06-02T10:00:32Z
day: '24'
doi: 10.1007/3-540-45828-X_9
extern: '1'
intvolume: '      2491'
language:
- iso: eng
month: '10'
oa_version: None
page: 108 - 122
publication: Proceedings of the 2nd International Conference on Embedded Software
publication_identifier:
  isbn:
  - '9783540443070'
publication_status: published
publisher: ACM
publist_id: '76'
quality_controlled: '1'
status: public
title: Timed interfaces
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2491
year: '2002'
...
---
_id: '4421'
abstract:
- lang: eng
  text: We demonstrate the feasibility and benefits of Giotto-based control software
    development by reimplementing the autopilot system of an autonomously flying model
    helicopter. Giotto offers a clean separation between the platform-independent
    concerns of software functionality and I/O timing, and the platform-dependent
    concerns of software scheduling and execution. Functionality code such as code
    computing control laws can be generated automatically from Simulink models or,
    as in the case of this project, inherited from a legacy system. I/O timing code
    is generated automatically from Giotto models that specify real-time requirements
    such as task frequencies and actuator update rates. We extend Simulink to support
    the design of Giotto models, and from these models, the automatic generation of
    Giotto code that supervises the interaction of the functionality code with the
    physical environment. The Giotto compiler performs a schedulability analysis on
    the Giotto code, and generates timing code for the helicopter platform. The Giotto
    methodology guarantees the stringent hard real-time requirements of the autopilot
    system, and at the same time supports the automation of the software development
    process in a way that produces a transparent software architecture with predictable
    behavior and reusable components.
acknowledgement: This research was supported in part by the DARPA SEC grant F33615-C-98-3614,
  the MARCO GSRC grant 98-DT-660, and the AFOSR MURI grant F49620-00-1-0327.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Christoph
  full_name: Kirsch, Christoph
  last_name: Kirsch
- first_name: Marco
  full_name: Sanvido, Marco
  last_name: Sanvido
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Wolfgang
  full_name: Pree, Wolfgang
  last_name: Pree
citation:
  ama: 'Kirsch C, Sanvido M, Henzinger TA, Pree W. A Giotto-based helicopter control
    system. In: <i>Proceedings of the 2nd International Conference on Embedded Software</i>.
    Vol 2491. ACM; 2002:46-60. doi:<a href="https://doi.org/10.1007/3-540-45828-X_5">10.1007/3-540-45828-X_5</a>'
  apa: 'Kirsch, C., Sanvido, M., Henzinger, T. A., &#38; Pree, W. (2002). A Giotto-based
    helicopter control system. In <i>Proceedings of the 2nd International Conference
    on Embedded Software</i> (Vol. 2491, pp. 46–60). Grenoble, France: ACM. <a href="https://doi.org/10.1007/3-540-45828-X_5">https://doi.org/10.1007/3-540-45828-X_5</a>'
  chicago: Kirsch, Christoph, Marco Sanvido, Thomas A Henzinger, and Wolfgang Pree.
    “A Giotto-Based Helicopter Control System.” In <i>Proceedings of the 2nd International
    Conference on Embedded Software</i>, 2491:46–60. ACM, 2002. <a href="https://doi.org/10.1007/3-540-45828-X_5">https://doi.org/10.1007/3-540-45828-X_5</a>.
  ieee: C. Kirsch, M. Sanvido, T. A. Henzinger, and W. Pree, “A Giotto-based helicopter
    control system,” in <i>Proceedings of the 2nd International Conference on Embedded
    Software</i>, Grenoble, France, 2002, vol. 2491, pp. 46–60.
  ista: 'Kirsch C, Sanvido M, Henzinger TA, Pree W. 2002. A Giotto-based helicopter
    control system. Proceedings of the 2nd International Conference on Embedded Software.
    EMSOFT: Embedded Software , LNCS, vol. 2491, 46–60.'
  mla: Kirsch, Christoph, et al. “A Giotto-Based Helicopter Control System.” <i>Proceedings
    of the 2nd International Conference on Embedded Software</i>, vol. 2491, ACM,
    2002, pp. 46–60, doi:<a href="https://doi.org/10.1007/3-540-45828-X_5">10.1007/3-540-45828-X_5</a>.
  short: C. Kirsch, M. Sanvido, T.A. Henzinger, W. Pree, in:, Proceedings of the 2nd
    International Conference on Embedded Software, ACM, 2002, pp. 46–60.
conference:
  end_date: 2002-10-09
  location: Grenoble, France
  name: 'EMSOFT: Embedded Software '
  start_date: 2002-10-07
date_created: 2018-12-11T12:08:46Z
date_published: 2002-09-25T00:00:00Z
date_updated: 2023-06-05T13:07:20Z
day: '25'
doi: 10.1007/3-540-45828-X_5
extern: '1'
intvolume: '      2491'
language:
- iso: eng
month: '09'
oa_version: None
page: 46 - 60
publication: Proceedings of the 2nd International Conference on Embedded Software
publication_identifier:
  isbn:
  - '9783540443070'
publication_status: published
publisher: ACM
publist_id: '310'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A Giotto-based helicopter control system
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2491
year: '2002'
...
---
_id: '4470'
abstract:
- lang: eng
  text: Giotto is a platform-independent language for specifying software for high-performance
    control applications. In this paper we present a new approach to the compilation
    of Giotto. Following this approach, the Giotto compiler generates code for a virtual
    machine, called the E machine, which can be ported to different platforms. The
    Giotto compiler also checks if the generated E code is time safe for a given platform,
    that is, if the platform offers sufficient performance to ensure that the E code
    is executed in a timely fashion that conforms with the Giotto semantics. Time-safety
    checking requires a schedulability analysis. We show that while for arbitrary
    E code, the analysis is exponential, for E code generated from typical Giotto
    programs, the analysis is polynomial. This supports our claim that Giotto identifies
    a useful fragment of embedded programs.
acknowledgement: Supported in part by the DARPA SEC grant F33615-C-98-3614, MARCO
  GSRC grant 98-DT-660, AFOSR MURI grant F49620-00-1-0327, NSF grant CCR-9988172,
  and a Microsoft Research Fellowship.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Christoph
  full_name: Kirsch, Christoph
  last_name: Kirsch
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Slobodan
  full_name: Matic, Slobodan
  last_name: Matic
citation:
  ama: 'Henzinger TA, Kirsch C, Majumdar R, Matic S. Time-safety checking for embedded
    programs. In: <i>Proceedings of the 2nd International Conference on Embedded Software</i>.
    Vol 2491. ACM; 2002:76-92. doi:<a href="https://doi.org/10.1007/3-540-45828-X_7">10.1007/3-540-45828-X_7</a>'
  apa: 'Henzinger, T. A., Kirsch, C., Majumdar, R., &#38; Matic, S. (2002). Time-safety
    checking for embedded programs. In <i>Proceedings of the 2nd International Conference
    on Embedded Software</i> (Vol. 2491, pp. 76–92). Grenoble, France: ACM. <a href="https://doi.org/10.1007/3-540-45828-X_7">https://doi.org/10.1007/3-540-45828-X_7</a>'
  chicago: Henzinger, Thomas A, Christoph Kirsch, Ritankar Majumdar, and Slobodan
    Matic. “Time-Safety Checking for Embedded Programs.” In <i>Proceedings of the
    2nd International Conference on Embedded Software</i>, 2491:76–92. ACM, 2002.
    <a href="https://doi.org/10.1007/3-540-45828-X_7">https://doi.org/10.1007/3-540-45828-X_7</a>.
  ieee: T. A. Henzinger, C. Kirsch, R. Majumdar, and S. Matic, “Time-safety checking
    for embedded programs,” in <i>Proceedings of the 2nd International Conference
    on Embedded Software</i>, Grenoble, France, 2002, vol. 2491, pp. 76–92.
  ista: 'Henzinger TA, Kirsch C, Majumdar R, Matic S. 2002. Time-safety checking for
    embedded programs. Proceedings of the 2nd International Conference on Embedded
    Software. EMSOFT: Embedded Software , LNCS, vol. 2491, 76–92.'
  mla: Henzinger, Thomas A., et al. “Time-Safety Checking for Embedded Programs.”
    <i>Proceedings of the 2nd International Conference on Embedded Software</i>, vol.
    2491, ACM, 2002, pp. 76–92, doi:<a href="https://doi.org/10.1007/3-540-45828-X_7">10.1007/3-540-45828-X_7</a>.
  short: T.A. Henzinger, C. Kirsch, R. Majumdar, S. Matic, in:, Proceedings of the
    2nd International Conference on Embedded Software, ACM, 2002, pp. 76–92.
conference:
  end_date: 2002-10-09
  location: Grenoble, France
  name: 'EMSOFT: Embedded Software '
  start_date: 2002-10-07
date_created: 2018-12-11T12:09:01Z
date_published: 2002-09-25T00:00:00Z
date_updated: 2023-06-05T08:50:59Z
day: '25'
doi: 10.1007/3-540-45828-X_7
extern: '1'
intvolume: '      2491'
language:
- iso: eng
month: '09'
oa_version: None
page: 76 - 92
publication: Proceedings of the 2nd International Conference on Embedded Software
publication_identifier:
  isbn:
  - '9783540443070'
publication_status: published
publisher: ACM
publist_id: '259'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Time-safety checking for embedded programs
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2491
year: '2002'
...