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 proceedingConference 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 languageEnglish
Title of host publicationLecture Notes in Electrical Engineering
Pages293-300
Number of pages8
Volume181 LNEE
DOIs
Publication statusPublished - 2012 Oct 19
Event7th International Conference on Embedded and Multimedia Computing, EMC 2012 - Gwangju, Korea, Republic of
Duration: 2012 Sep 62012 Sep 8

Publication series

NameLecture Notes in Electrical Engineering
Volume181 LNEE
ISSN (Print)18761100
ISSN (Electronic)18761119

Other

Other7th International Conference on Embedded and Multimedia Computing, EMC 2012
CountryKorea, Republic of
CityGwangju
Period12/9/612/9/8

Fingerprint

Hybrid systems
Differential equations
Specifications
Modeling languages
Formal verification

Keywords

  • ECML
  • Formal Verification
  • Hybrid System
  • Linear Hybrid Automata
  • Translation

ASJC Scopus subject areas

  • Industrial and Manufacturing Engineering

Cite this

Jo, J., Yoo, J., Choi, H., Cha, S., Lee, H. Y., & Kim, W. T. (2012). Translation from ECML to linear hybrid automata. In Lecture Notes in Electrical Engineering (Vol. 181 LNEE, pp. 293-300). (Lecture Notes in Electrical Engineering; Vol. 181 LNEE). https://doi.org/10.1007/978-94-007-5076-0_34

Translation from ECML to linear hybrid automata. / Jo, Jaeyeon; Yoo, Junbeom; Choi, Han; Cha, Sungdeok; Lee, Hae Young; Kim, Won Tae.

Lecture Notes in Electrical Engineering. Vol. 181 LNEE 2012. p. 293-300 (Lecture Notes in Electrical Engineering; Vol. 181 LNEE).

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

Jo, J, Yoo, J, Choi, H, Cha, S, Lee, HY & Kim, WT 2012, Translation from ECML to linear hybrid automata. in Lecture Notes in Electrical Engineering. vol. 181 LNEE, 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
Jo J, Yoo J, Choi H, Cha S, Lee HY, Kim WT. Translation from ECML to linear hybrid automata. In Lecture Notes in Electrical Engineering. Vol. 181 LNEE. 2012. p. 293-300. (Lecture Notes in Electrical Engineering). https://doi.org/10.1007/978-94-007-5076-0_34
Jo, Jaeyeon ; Yoo, Junbeom ; Choi, Han ; Cha, Sungdeok ; Lee, Hae Young ; Kim, Won Tae. / Translation from ECML to linear hybrid automata. Lecture Notes in Electrical Engineering. Vol. 181 LNEE 2012. pp. 293-300 (Lecture Notes in Electrical Engineering).
@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",
month = "10",
day = "19",
doi = "10.1007/978-94-007-5076-0_34",
language = "English",
isbn = "9789400750753",
volume = "181 LNEE",
series = "Lecture Notes in Electrical Engineering",
pages = "293--300",
booktitle = "Lecture Notes in Electrical Engineering",

}

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/10/19

Y1 - 2012/10/19

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

UR - http://www.scopus.com/inward/citedby.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

VL - 181 LNEE

T3 - Lecture Notes in Electrical Engineering

SP - 293

EP - 300

BT - Lecture Notes in Electrical Engineering

ER -