A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> In this paper we address the problem of distributing model checking of timed automata. We demonstrate through four real life examples that the combined processing and memory resources of multiprocessor computers can be effectively utilized. The approach assumes a distributed memory model and is applied to both a network of workstations and a symmetric multiprocessor machine. However, certain unexpected phenomena have to be taken into account. We show how in the timed case the search order of the state space is crucial for the effectiveness and scalability of the exploration. An effective heuristic to counter the effect of the search order is provided. Some of the results open up for improvements in the single processor case. <s> BIB001 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> In this paper we propose a distributed algorithm for model-checking LTL. In particular, we explore the possibility of performing nested depth-first search algorithm in distributed SPIN. A distributed version of the algorithm is presented, and its complexity is discussed. <s> BIB002 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> In this paper, a formal analysis of security protocols in the field of wireless sensor networks is presented. Three complementary protocols, TinySec, LEAP and TinyPK, are modelled using the high-level formal language HLPSL, and verified using the model checking tool AVISPA, where two main security properties are checked: authenticity and confidentiality of messages. As a result of this analysis, two attacks have been found: a man-in-the-middle-attack and a type flaw attack. In both cases confidentiality is compromised and an intruder may obtain confidential data from a node in the network. Two solutions to these attacks are proposed in the paper. <s> BIB003 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> Wireless sensor networks are often used by experts in many different fields to gather data pertinent to their work. Although their expertise may not include software engineering, these users are expected to produce low-level software for a concurrent, real-time and resource-constrained computing environment. In this paper, we introduce a component-based model for wireless sensor network applications and a language, Insense, for supporting the model. An application is modelled as a composition of interacting components and the application model is preserved in the Insense implementation where active components communicate via typed channels. The primary design criteria for Insense include: to abstract over low-level concerns for ease of programming; to permit worst-case space and time usage of programs to be determinable; to support the fractal composition of components whilst eliminating implicit dependencies between them; and, to facilitate the construction of low footprint programs suitable for resource-constrained devices. This paper presents an overview of the component model and Insense, and demonstrates how they meet the above criteria. <s> BIB004 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> The design and implementation of wireless sensor network applications often require domain experts, who may lack expertise in software engineering, to produce resource-constrained, concurrent, real-time software without the support of high-level software engineering facilities. The Insense language aims to address this mismatch by allowing the complexities of synchronisation, memory management and event-driven programming to be borne by the language implementation rather than by the programmer. The main contribution of this paper is an initial step towards verifying the correctness of WSN applications with a focus on concurrency. We model part of the synchronisation mechanism of the Insense language implementation using Promela constructs and verify its correctness using Spin . We demonstrate how a previously published version of the mechanism is shown to be incorrect by Spin , and give complete verification results for the revised mechanism. <s> BIB005 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> Along with the popularity of software-intensive systems, the interactions between system components and between humans and software applications are becoming more and more complex. This results in system accidents related to system safety issues. System accidents are different to failures related to component reliability. System safety is not well addressed, because functional requirements and safety requirements are separately handled in practice. In this paper, we consider safety requirements as control structures that restrict system behaviors at meta-model level. We propose the formalism of interface C-Systems, short for "interface control systems''. In this framework, functional requirements and safety requirements are separately formalized as interface automata and controlling automata respectively, as what we are doing in practice. The controlling automaton may guarantee safety requirements at design-time or runtime. Then the global system is a safe specification. The underlying mechanism differs from that of model checking. It explicitly separates the tasks of product engineers and safety engineers, and provides a new top-down methodology for designing and modeling a system with safety constraints, and for automatically composing a safe system that conforms to safety requirements. In practice, this methodology may be also used for safety checking, incident reporting and service restoration. <s> BIB006 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> We propose the nevertrace claim, which is a new construct for specifying the correctness properties that either finite or infinite execution traces (i.e., sequences of transitions) that should never occur. In semantics, it is neither similar to never claim and trace assertion, nor a simple combination of them. Furthermore, the theoretical foundation for checking nevertrace claims, namely the Asynchronous-Composition Buchi Automaton Control System (AC-BAC System), is proposed. The major contributions of the nevertrace claim include: a powerful construct for formalizing properties related to transitions and their labels, and a way for reducing the state space at the design stage. <s> BIB007 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> Several different secure routing protocols have been proposed for determining the appropriate paths on which data should be transmitted in ad hoc networks. In this paper, we focus on two of the most relevant such protocols, ARAN and end air A, and present the results of a formal analysis that we have carried out using the AVISPA Tool, an automated model checker for the analysis of security protocols. By model checking ARAN with the AVISPA Tool, we have discovered three attacks (a route disruption, a route diversion, and a creation of incorrect routing state), while our analysis of end air A revealed no attacks. <s> BIB008 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> The research is motivated by the challenge from the evolution of safety requirements, which leads to revision of system designs at design-time or post-implementation at a high cost. This paper proposes a complementary methodology, namely the model monitoring approach, to better support the evolution throughout the life-cycle at a lower cost. <s> BIB009 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> Radio Frequency IDentification (RFID) has attracted considerable attention in recent years for its low cost, general availability, and location sensing functionality. Most existing schemes require the tracked persons to be labeled with RFID tags. This requirement may not be satisfied for some activity sensing applications due to privacy and security concerns and uncertainty of objects to be monitored, e.g., group behavior monitoring in warehouses with privacy limitations, and abnormal customers in banks. In this paper, we propose TASA-Tag-free Activity Sensing using RFID tag Arrays for location sensing and frequent route detection. TASA relaxes the monitored objects from attaching RFID tags, online recovers and checks frequent trajectories by capturing the Received Signal Strength Indicator (RSSI) series for passive RFID tag arrays where objects traverse. In order to improve the accuracy for estimated trajectories and accelerate location sensing, TASA introduces reference tags with known positions. With the readings from reference tags, TASA can locate objects more accurately. Extensive experiment shows that TASA is an effective approach for certain activity sensing applications. <s> BIB010 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> Contexts are often inconsistent in pervasive computing environments, owing to many heterogeneous devices with limited processing capabilities, imperfect measurement techniques, and user movement. A variety of schemes have been proposed to check context inconsistency. However, they implicitly require central control. This requirement inhibits their effectiveness in some pervasive computing environments (e.g., transport systems) where all nodes are resource-constrained and cannot act as a centralized node. To this end, we propose in this paper DCCI--a scheme of Decentralized Checking of Context Inconsistency in pervasive computing environments. DCCI exploits a simple, yet efficient, preference-based locality that denotes nodes requiring that the same context can check the inconsistency on this type of contexts. According to this locality, DCCI constructs a preference-based shortcut structure such that it checks context inconsistency within the shortcut structure. Extensive experiments show that DCCI can accurately and efficiently check context inconsistency in the presence of node churns and heterogeneity. <s> BIB011 </s> A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks <s> Challenges and Future Work <s> Event detection for context inconsistency is challenging in pervasive computing environments, where contexts are often noisy owing to fragile connectivity, node frequent movement and resource constraints. As a recent scheme, CEDA - Concurrent Event Detection for Asynchronous inconsistency checking (CEDA) - concurrently detects context inconsistency by exploring the happened-before relation among events. Nevertheless, CEDA suffers from several problems - unscalable from partial centralised detection manner, heavy computation complexity and false negative. To address these challenges, we propose in this paper the SECA scheme - asynchronous event detection for context inconsistency in pervasive computing. It puts forward a new type logical clock - snapshot timestamp - to check event relations, which enables it to be efficient in the scenarios where CEDA fails to. Meanwhile, SECA comes up with a lightweight update mechanism for the snapshot clock, which considerably reduces time and space complexity. Extensive experiments have been conducted and results show that SECA surmounts CEDA with respect to detection accuracy and scalability. <s> BIB012
As we know, the biggest challenge comes from the model checking algorithms, which generate a huge and intractable state space in checking. To address this issue, new improvements of checking algorithms are being developed to reduce the state space, such as BIB007 . And some parallel model checking algorithms have been proposed recently BIB001 BIB002 . Extending existing verification tools with distributed checking algorithms may gain higher speed and better performance. This may enable the automatic checking of larger fixed networks and a wider range of scenarios. Another challenge could be enhancing the automation level of theorem provers. Currently, most engineers are not capable of using provers, due to the lack of enough mathematical knowledge on that. Less user interaction may accelerate the application of theorem provers in industrial verification practice. Challenge also comes from the engineers' expectation that the verification should be done on the real implementations of protocols such as codes, rather than on the models. As we know, subtle but fatal faults may be introduced, even when we are implementing a verified correct model. Direct checking of real codes would be more attractive and useful to engineers, since it can fill the gap between the model and the implementation of a protocol. In the future, we may study how to assure the security of routing protocols, which is related to but different from the correctness and reliability of routing protocols that have been discussed in this survey. Some recent works tried to explore the approaches for model checking wireless sensor network security protocols, in order to decide the existence of attacks, such as route disruption, route diversion etc. BIB003 BIB008 . Another future direction could be the development of the languages for constructing wireless sensor network applications. A recent work introduced such a language named Insense, which supports a component-based model for wireless sensor network applications, and can facilitate the construction of low-level software for a concurrent, real-time and resource-constrained computing environment BIB004 . Furthermore, the correctness of the implementations of send and receive operations was verified using SPIN on some typical small network models consisting of less than four nodes BIB005 . Finally, we may also explore other techniques for verifying protocols such as runtime monitoring and control BIB009 BIB006 , and their theoretical foundations like ω-automata  . We will try to apply these techniques to real-world applications like RFID networks BIB010 and pervasive computing environments BIB011 BIB012 .