@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 = "美国",
}