2008 11th IEEE Symposium on Object Oriented Real-Time Distributed Computing (ISORC) Model Checking Multi-Task Software on Real-Time Operating Systems May 05-May 07 ISBN: 978-0-7695-3132-8
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ISORC.2008.46
In this paper, we propose a method to verify software executed on RTOS which conforms to micro ITRON with a model checking tool Spin. The RTOS provides facilities such as priorities and service calls to controlthe execution of tasks, however, Spin does not provide them. Thus, we implemented a middleware which allows us to use the facilities and simulate the execution of the tasks in Spin. The paper shows how it is implemented and its evaluation.
Citation:
Toshiaki Aoki, "Model Checking Multi-Task Software on Real-Time Operating Systems," isorc, pp.551-555, 2008 11th IEEE Symposium on Object Oriented Real-Time Distributed Computing (ISORC), 2008 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb