Proof-based formal methods for WSN development with Simulation Approach

摘要

Software engineering (SE) plays a fundamental role in wireless sensor network (WSN) development due to the appearance of WSN adoption over wide range of the real-world physical applications. The WSN software development process focuses on “low phases” of development such as programming, testing and deployment. In current practice, programmers decompose the problem and then develop code for sensor nodes based on the functionality provided by the operating system platform of choice before integrating with low level hardware. The current WSN development process is performed under very limited OS or development resource available. Simulation testing, emulation testing and laboratory testbed techniques are the main approaches to analyse and evaluate the correctness and performance of network algorithms and protocols. However, since WSNs have been applied to safety-critical application domains from healthcare to military applications, the high-level abstraction and verification and validation techniques have become an important key for current WSN development. It is quite evident that they lack SE methods, techniques and tools which support “high phases" of current practices on WSN development such as requirements and architecture specification. This research proposes a hybrid verification and validation approach for the “high phases” of WSN development process by integrating formal methods with existing simulation technologies.