The Community for Technology Leaders
Secure Software Integration and Reliability Improvement Companion, IEEE International Conference on (2010)
Singapore, Singapore
June 9, 2010 to June 11, 2010
ISBN: 978-0-7695-4087-0
pp: 7-12
ABSTRACT
The programming language nesC for TinyOS applications supports special features of sensor network systems by providing a component-oriented programming model which is flexibly concurrent/reactive and event-driven. Sensor network systems are correctness critical since they are expected to work autonomously. Formal verification techniques such as model checking have been successfully applied to assure the reliability and correctness of concurrent systems and real-time systems. However, manually constructing a formal model is always a non-trivial task. We develop a lightweight framework for sensor network systems which automatically extracts real-time models from nesC implementations and verifies them against goals using model checking techniques. We believe that our approach contributes to systematically improving the quality of sensor network systems, with little overhead or cost caused by applying verification techniques.
INDEX TERMS
Sensor Network System, Model Checking, RTS
CITATION
Man Chun Zheng, "An Automatic Approach to Verify Sensor Network Systems", Secure Software Integration and Reliability Improvement Companion, IEEE International Conference on, vol. 00, no. , pp. 7-12, 2010, doi:10.1109/SSIRI-C.2010.12
87 ms
(Ver 3.3 (11022016))