A timed CSP model for the time-triggered language Giotto

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.