Translation from ECML to linear hybrid automata

Jaeyeon Jo; Junbeom Yoo; Han Choi; Sungdeok Cha; Hae Young Lee; Won Tae Kim

doi:10.1007/978-94-007-5076-0_34

Translation from ECML to linear hybrid automata

Jaeyeon Jo, Junbeom Yoo, Han Choi, Sungdeok Cha, Hae Young Lee, Won Tae Kim

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

1 Citation (Scopus)

Abstract

ECML (ETRI CPS Modeling Language) is a modeling formalism for hybrid systems, recently proposed by a research institute - ETRI in Korea. It extends a basic formalism DEV&DESS (Discrete EVent & Differential Equation System Specification) with various conveniences in modeling and simulation. The formal verification tool for ECML has not been provided yet. This paper proposes translation rules from ECML to linear hybrid automata which is an input front-end of HyTech. We can verify ECML models with the HyTech model checker.

Original language	English
Title of host publication	Embedded and Multimedia Computing Technology and Service, EMC 2012
Pages	293-300
Number of pages	8
DOIs	https://doi.org/10.1007/978-94-007-5076-0_34
Publication status	Published - 2012
Event	7th International Conference on Embedded and Multimedia Computing, EMC 2012 - Gwangju, Korea, Republic of Duration: 2012 Sept 6 → 2012 Sept 8

Publication series

Name	Lecture Notes in Electrical Engineering
Volume	181 LNEE
ISSN (Print)	1876-1100
ISSN (Electronic)	1876-1119

Other

Other	7th International Conference on Embedded and Multimedia Computing, EMC 2012
Country/Territory	Korea, Republic of
City	Gwangju
Period	12/9/6 → 12/9/8

Keywords

ECML
Formal Verification
Hybrid System
Linear Hybrid Automata
Translation

ASJC Scopus subject areas

Industrial and Manufacturing Engineering

Access to Document

10.1007/978-94-007-5076-0_34

Cite this

Jo, J, Yoo, J, Choi, H, Cha, S, Lee, HY & Kim, WT 2012, Translation from ECML to linear hybrid automata. in Embedded and Multimedia Computing Technology and Service, EMC 2012. Lecture Notes in Electrical Engineering, vol. 181 LNEE, pp. 293-300, 7th International Conference on Embedded and Multimedia Computing, EMC 2012, Gwangju, Korea, Republic of, 12/9/6. https://doi.org/10.1007/978-94-007-5076-0_34

@inproceedings{bfa5fc3bf91d403f93d1a63d43d9499d,

title = "Translation from ECML to linear hybrid automata",

abstract = "ECML (ETRI CPS Modeling Language) is a modeling formalism for hybrid systems, recently proposed by a research institute - ETRI in Korea. It extends a basic formalism DEV&DESS (Discrete EVent & Differential Equation System Specification) with various conveniences in modeling and simulation. The formal verification tool for ECML has not been provided yet. This paper proposes translation rules from ECML to linear hybrid automata which is an input front-end of HyTech. We can verify ECML models with the HyTech model checker.",

keywords = "ECML, Formal Verification, Hybrid System, Linear Hybrid Automata, Translation",

author = "Jaeyeon Jo and Junbeom Yoo and Han Choi and Sungdeok Cha and Lee, {Hae Young} and Kim, {Won Tae}",

year = "2012",

doi = "10.1007/978-94-007-5076-0_34",

language = "English",

isbn = "9789400750753",

series = "Lecture Notes in Electrical Engineering",

pages = "293--300",

booktitle = "Embedded and Multimedia Computing Technology and Service, EMC 2012",

note = "7th International Conference on Embedded and Multimedia Computing, EMC 2012 ; Conference date: 06-09-2012 Through 08-09-2012",

}

TY - GEN

T1 - Translation from ECML to linear hybrid automata

AU - Jo, Jaeyeon

AU - Yoo, Junbeom

AU - Choi, Han

AU - Cha, Sungdeok

AU - Lee, Hae Young

AU - Kim, Won Tae

PY - 2012

Y1 - 2012

N2 - ECML (ETRI CPS Modeling Language) is a modeling formalism for hybrid systems, recently proposed by a research institute - ETRI in Korea. It extends a basic formalism DEV&DESS (Discrete EVent & Differential Equation System Specification) with various conveniences in modeling and simulation. The formal verification tool for ECML has not been provided yet. This paper proposes translation rules from ECML to linear hybrid automata which is an input front-end of HyTech. We can verify ECML models with the HyTech model checker.

AB - ECML (ETRI CPS Modeling Language) is a modeling formalism for hybrid systems, recently proposed by a research institute - ETRI in Korea. It extends a basic formalism DEV&DESS (Discrete EVent & Differential Equation System Specification) with various conveniences in modeling and simulation. The formal verification tool for ECML has not been provided yet. This paper proposes translation rules from ECML to linear hybrid automata which is an input front-end of HyTech. We can verify ECML models with the HyTech model checker.

KW - ECML

KW - Formal Verification

KW - Hybrid System

KW - Linear Hybrid Automata

KW - Translation

UR - http://www.scopus.com/inward/record.url?scp=84867461115&partnerID=8YFLogxK

U2 - 10.1007/978-94-007-5076-0_34

DO - 10.1007/978-94-007-5076-0_34

M3 - Conference contribution

AN - SCOPUS:84867461115

SN - 9789400750753

T3 - Lecture Notes in Electrical Engineering

SP - 293

EP - 300

BT - Embedded and Multimedia Computing Technology and Service, EMC 2012

T2 - 7th International Conference on Embedded and Multimedia Computing, EMC 2012

Y2 - 6 September 2012 through 8 September 2012

ER -

Translation from ECML to linear hybrid automata

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this