A Timed CSP Model for the Time-Triggered Language Giotto

Yanhong Huang, Yongxin Zhao, Shengchao Qin, Guanhua He, Joao Ferreira

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    Giotto is a time-triggered embedded programming language which provides an abstract programming model for hard real-time applications. It effectively decouples the implementation from the design. A Giotto program focuses on the functionality and timing of periodic tasks. All the actions, e.g., task invocations, actuator updates, and mode switches, described in Giotto programs are triggered by real time. We take the views of the concerns of Giotto programs, including the reaction to the environment, the communication between tasks, the timing predictability, etc. Our goal is to simulate Giotto programs using a timed CSP-based model which can effectively express the concerns and can be used to verify safety properties. This paper is a first step that presents the timed CSP model for Giotto programs. We also give a case study to illustrate the utility of the timed CSP model. Based on the existing research for CSP with time, we believe that our model can support to analyze and verify safety properties of Giotto programs.
    Original languageEnglish
    Title of host publication2012 35th Annual IEEE Software Engineering Workshop
    ISBN (Print)9781467355742
    Publication statusPublished - 2012
    Event35th Annual IEEE Software Engineering Workshop - Heraclion, Greece
    Duration: 12 Oct 201213 Oct 2012
    Conference number: 35


    Conference35th Annual IEEE Software Engineering Workshop
    Abbreviated titleSEW 2012


    Dive into the research topics of 'A Timed CSP Model for the Time-Triggered Language Giotto'. Together they form a unique fingerprint.

    Cite this