A timed CSP model for the time-triggered language Giotto

Yanhong Huang; Yongxin Zhao; Shengchao Qin; Guanhua He; João F. Ferreira

doi:10.1109/SEW.2012.18

A timed CSP model for the time-triggered language Giotto

Yanhong Huang^*
, Yongxin Zhao
, Shengchao Qin
, Guanhua He
, João F. Ferreira

^*Corresponding author for this work

Software Engineering Institute

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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 language	English
Title of host publication	Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012
Pages	110-119
Number of pages	10
DOIs	https://doi.org/10.1109/SEW.2012.18
State	Published - 2012
Event	2012 IEEE 35th Software Engineering Workshop, SEW 2012 - Heraklion, Crete, Greece Duration: 12 Oct 2012 → 13 Oct 2012

Publication series

Name	Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012

Conference

Conference	2012 IEEE 35th Software Engineering Workshop, SEW 2012
Country/Territory	Greece
City	Heraklion, Crete
Period	12/10/12 → 13/10/12

Keywords

Embedded systems
Giotto
Simulation
Time-triggered language
Timed CSP

Access to Document

10.1109/SEW.2012.18

Cite this

@inproceedings{44bbaca11c9349439763b70d318d88e1,

title = "A timed CSP model for the time-triggered language Giotto",

abstract = "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.",

keywords = "Embedded systems, Giotto, Simulation, Time-triggered language, Timed CSP",

author = "Yanhong Huang and Yongxin Zhao and Shengchao Qin and Guanhua He and Ferreira, \{Jo{\~a}o F.\}",

year = "2012",

doi = "10.1109/SEW.2012.18",

language = "英语",

isbn = "9780769549477",

series = "Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012",

pages = "110--119",

booktitle = "Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012",

note = "2012 IEEE 35th Software Engineering Workshop, SEW 2012 ; Conference date: 12-10-2012 Through 13-10-2012",

}

Huang, Y , Zhao, Y, Qin, S, He, G & Ferreira, JF 2012, A timed CSP model for the time-triggered language Giotto. in Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012., 6479808, Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012, pp. 110-119, 2012 IEEE 35th Software Engineering Workshop, SEW 2012, Heraklion, Crete, Greece, 12/10/12. https://doi.org/10.1109/SEW.2012.18

A timed CSP model for the time-triggered language Giotto. / Huang, Yanhong ; Zhao, Yongxin; Qin, Shengchao et al.
Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012. 2012. p. 110-119 6479808 (Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A timed CSP model for the time-triggered language Giotto

AU - Huang, Yanhong

AU - Zhao, Yongxin

AU - Qin, Shengchao

AU - He, Guanhua

AU - Ferreira, João F.

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

KW - Embedded systems

KW - Giotto

KW - Simulation

KW - Time-triggered language

KW - Timed CSP

UR - https://www.scopus.com/pages/publications/84876108607

U2 - 10.1109/SEW.2012.18

DO - 10.1109/SEW.2012.18

M3 - 会议稿件

AN - SCOPUS:84876108607

SN - 9780769549477

T3 - Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012

SP - 110

EP - 119

BT - Proceedings of the 2012 IEEE 35th Software Engineering Workshop, SEW 2012

T2 - 2012 IEEE 35th Software Engineering Workshop, SEW 2012

Y2 - 12 October 2012 through 13 October 2012

ER -

A timed CSP model for the time-triggered language Giotto

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this