[{"conference":{"location":"Grenoble, France","end_date":"2002-10-09","start_date":"2002-10-07","name":"EMSOFT: Embedded Software "},"language":[{"iso":"eng"}],"month":"10","oa_version":"None","publication":"Proceedings of the 2nd International Conference on Embedded Software","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"76","publication_identifier":{"isbn":["9783540443070"]},"date_published":"2002-10-24T00:00:00Z","type":"conference","publisher":"ACM","page":"108 - 122","quality_controlled":"1","alternative_title":["LNCS"],"title":"Timed interfaces","intvolume":"      2491","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:51Z","author":[{"full_name":"De Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mariëlle","last_name":"Stoelinga","full_name":"Stoelinga, Mariëlle"}],"_id":"4631","extern":"1","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.","volume":2491,"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."}],"doi":"10.1007/3-540-45828-X_9","day":"24","date_updated":"2023-06-02T10:00:32Z","year":"2002","citation":{"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>","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>","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.","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>.","short":"L. De Alfaro, T.A. Henzinger, M. Stoelinga, in:, Proceedings of the 2nd International Conference on Embedded Software, ACM, 2002, pp. 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>.","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."}},{"type":"conference","date_published":"2002-09-25T00:00:00Z","publication_identifier":{"isbn":["9783540443070"]},"publist_id":"310","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","publication":"Proceedings of the 2nd International Conference on Embedded Software","oa_version":"None","month":"09","language":[{"iso":"eng"}],"conference":{"start_date":"2002-10-07","name":"EMSOFT: Embedded Software ","location":"Grenoble, France","end_date":"2002-10-09"},"citation":{"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.","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>.","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.","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>","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>","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.","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>."},"year":"2002","date_updated":"2023-06-05T13:07:20Z","day":"25","doi":"10.1007/3-540-45828-X_5","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.","volume":2491,"extern":"1","scopus_import":"1","_id":"4421","author":[{"full_name":"Kirsch, Christoph","first_name":"Christoph","last_name":"Kirsch"},{"full_name":"Sanvido, Marco","last_name":"Sanvido","first_name":"Marco"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Pree","first_name":"Wolfgang","full_name":"Pree, Wolfgang"}],"date_created":"2018-12-11T12:08:46Z","article_processing_charge":"No","publication_status":"published","intvolume":"      2491","alternative_title":["LNCS"],"title":"A Giotto-based helicopter control system","quality_controlled":"1","page":"46 - 60","publisher":"ACM"},{"date_published":"2002-09-25T00:00:00Z","type":"conference","publication_identifier":{"isbn":["9783540443070"]},"publist_id":"259","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication":"Proceedings of the 2nd International Conference on Embedded Software","oa_version":"None","month":"09","language":[{"iso":"eng"}],"conference":{"name":"EMSOFT: Embedded Software ","start_date":"2002-10-07","location":"Grenoble, France","end_date":"2002-10-09"},"date_updated":"2023-06-05T08:50:59Z","year":"2002","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.","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.","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."},"doi":"10.1007/3-540-45828-X_7","day":"25","abstract":[{"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.","lang":"eng"}],"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.","volume":2491,"extern":"1","_id":"4470","scopus_import":"1","author":[{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Christoph","last_name":"Kirsch","full_name":"Kirsch, Christoph"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"full_name":"Matic, Slobodan","first_name":"Slobodan","last_name":"Matic"}],"publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:01Z","title":"Time-safety checking for embedded programs","alternative_title":["LNCS"],"intvolume":"      2491","page":"76 - 92","quality_controlled":"1","publisher":"ACM"}]