Evaluation of Maude as a test generation engine for automotive operating systems

Yunja Choi; Min Zhang; Kazuhiro Ogatay

doi:10.1109/APSEC.2014.52

Evaluation of Maude as a test generation engine for automotive operating systems

Yunja Choi, Min Zhang, Kazuhiro Ogatay

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

1 Scopus citations

Abstract

This work evaluates Maude, an expressive and executable algebraic specification language, as a potential test sequence generation engine in the context of constraint-based test sequence generation for automotive operating systems. Our approach defines requirement specifications for automotive operating systems compliant with the OSEK/VDX international standard, and specifies constraint patterns in Maude. The correctness of the Maude specification is verified using LTL model checking and the test sequences from each classified environment are generated using reachability computation provided by the Maude rewriting engine. Experimental evaluation shows that constraintbased test generation using Maude can be as effective as that of using NuSMV, a statemachine based specification language specialized for model checking and specification-based testing, but more expressive and flexible.

Original language	English
Title of host publication	Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014
Editors	Yann-Gael Gueheneuc, Gihwon Kwon, Sungdeok Cha
Publisher	IEEE Computer Society
Pages	295-302
Number of pages	8
ISBN (Electronic)	9781479974252
DOIs	https://doi.org/10.1109/APSEC.2014.52
State	Published - 2014
Externally published	Yes
Event	21st Asia-Pacific Software Engineering Conference, APSEC 2014 - Jeju Island, Korea, Republic of Duration: 1 Dec 2014 → 4 Dec 2014

Publication series

Name	Proceedings - Asia-Pacific Software Engineering Conference, APSEC
Volume	1
ISSN (Print)	1530-1362

Conference

Conference	21st Asia-Pacific Software Engineering Conference, APSEC 2014
Country/Territory	Korea, Republic of
City	Jeju Island
Period	1/12/14 → 4/12/14

Keywords

Maude
NuSMV
OSEK/VDX
Safety testing.

Access to Document

10.1109/APSEC.2014.52

Cite this

Choi, Y., Zhang, M., & Ogatay, K. (2014). Evaluation of Maude as a test generation engine for automotive operating systems. In Y.-G. Gueheneuc, G. Kwon, & S. Cha (Eds.), Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014 (pp. 295-302). Article 7091323 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 1). IEEE Computer Society. https://doi.org/10.1109/APSEC.2014.52

Choi, Yunja ; Zhang, Min ; Ogatay, Kazuhiro. / Evaluation of Maude as a test generation engine for automotive operating systems. Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014. editor / Yann-Gael Gueheneuc ; Gihwon Kwon ; Sungdeok Cha. IEEE Computer Society, 2014. pp. 295-302 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC).

@inproceedings{8240cf98c99b4383bd21ab40ea915353,

title = "Evaluation of Maude as a test generation engine for automotive operating systems",

abstract = "This work evaluates Maude, an expressive and executable algebraic specification language, as a potential test sequence generation engine in the context of constraint-based test sequence generation for automotive operating systems. Our approach defines requirement specifications for automotive operating systems compliant with the OSEK/VDX international standard, and specifies constraint patterns in Maude. The correctness of the Maude specification is verified using LTL model checking and the test sequences from each classified environment are generated using reachability computation provided by the Maude rewriting engine. Experimental evaluation shows that constraintbased test generation using Maude can be as effective as that of using NuSMV, a statemachine based specification language specialized for model checking and specification-based testing, but more expressive and flexible.",

keywords = "Maude, NuSMV, OSEK/VDX, Safety testing.",

author = "Yunja Choi and Min Zhang and Kazuhiro Ogatay",

note = "Publisher Copyright: {\textcopyright} 2014 IEEE.; 21st Asia-Pacific Software Engineering Conference, APSEC 2014 ; Conference date: 01-12-2014 Through 04-12-2014",

year = "2014",

doi = "10.1109/APSEC.2014.52",

language = "英语",

series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",

publisher = "IEEE Computer Society",

pages = "295--302",

editor = "Yann-Gael Gueheneuc and Gihwon Kwon and Sungdeok Cha",

booktitle = "Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014",

address = "美国",

}

Choi, Y, Zhang, M & Ogatay, K 2014, Evaluation of Maude as a test generation engine for automotive operating systems. in Y-G Gueheneuc, G Kwon & S Cha (eds), Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014., 7091323, Proceedings - Asia-Pacific Software Engineering Conference, APSEC, vol. 1, IEEE Computer Society, pp. 295-302, 21st Asia-Pacific Software Engineering Conference, APSEC 2014, Jeju Island, Korea, Republic of, 1/12/14. https://doi.org/10.1109/APSEC.2014.52

Evaluation of Maude as a test generation engine for automotive operating systems. / Choi, Yunja; Zhang, Min; Ogatay, Kazuhiro.
Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014. ed. / Yann-Gael Gueheneuc; Gihwon Kwon; Sungdeok Cha. IEEE Computer Society, 2014. p. 295-302 7091323 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 1).

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

TY - GEN

T1 - Evaluation of Maude as a test generation engine for automotive operating systems

AU - Choi, Yunja

AU - Zhang, Min

AU - Ogatay, Kazuhiro

PY - 2014

Y1 - 2014

N2 - This work evaluates Maude, an expressive and executable algebraic specification language, as a potential test sequence generation engine in the context of constraint-based test sequence generation for automotive operating systems. Our approach defines requirement specifications for automotive operating systems compliant with the OSEK/VDX international standard, and specifies constraint patterns in Maude. The correctness of the Maude specification is verified using LTL model checking and the test sequences from each classified environment are generated using reachability computation provided by the Maude rewriting engine. Experimental evaluation shows that constraintbased test generation using Maude can be as effective as that of using NuSMV, a statemachine based specification language specialized for model checking and specification-based testing, but more expressive and flexible.

AB - This work evaluates Maude, an expressive and executable algebraic specification language, as a potential test sequence generation engine in the context of constraint-based test sequence generation for automotive operating systems. Our approach defines requirement specifications for automotive operating systems compliant with the OSEK/VDX international standard, and specifies constraint patterns in Maude. The correctness of the Maude specification is verified using LTL model checking and the test sequences from each classified environment are generated using reachability computation provided by the Maude rewriting engine. Experimental evaluation shows that constraintbased test generation using Maude can be as effective as that of using NuSMV, a statemachine based specification language specialized for model checking and specification-based testing, but more expressive and flexible.

KW - Maude

KW - NuSMV

KW - OSEK/VDX

KW - Safety testing.

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

U2 - 10.1109/APSEC.2014.52

DO - 10.1109/APSEC.2014.52

M3 - 会议稿件

AN - SCOPUS:84951287085

T3 - Proceedings - Asia-Pacific Software Engineering Conference, APSEC

SP - 295

EP - 302

BT - Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014

A2 - Gueheneuc, Yann-Gael

A2 - Kwon, Gihwon

A2 - Cha, Sungdeok

PB - IEEE Computer Society

T2 - 21st Asia-Pacific Software Engineering Conference, APSEC 2014

Y2 - 1 December 2014 through 4 December 2014

ER -

Choi Y, Zhang M, Ogatay K. Evaluation of Maude as a test generation engine for automotive operating systems. In Gueheneuc YG, Kwon G, Cha S, editors, Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014. IEEE Computer Society. 2014. p. 295-302. 7091323. (Proceedings - Asia-Pacific Software Engineering Conference, APSEC). doi: 10.1109/APSEC.2014.52

Evaluation of Maude as a test generation engine for automotive operating systems

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this