著者

CHOI Yunja

出版者

The Institute of Electronics, Information and Communication Engineers

雑誌

IEICE transactions on information and systems (ISSN:09168532)

巻号頁・発行日

vol.96, no.3, pp.735-738, 2013-03-01

被引用文献数

1

---

An automotive operating system is a typical safety-critical software and therefore requires extensive analysis w.r.t its effect on system safety. Our earlier work [1] reported a systematic model checking approach for checking the safety properties of the OSEK/VDX-based operating system Trampoline. This article reports further performance improvement using embeddedC constructs for efficient verification of the Trampoline model developed in the earlier work. Experiments show that the use of embeddedC constructs greatly reduces verification costs.