Formal Verification of Mobile Agent Based Anomaly Detection in Wireless Sensor Networks
Author(s)
Usman, Muhammad
Muthukkumarasamy, Vallipuram
Wu, Xin-Wen
Griffith University Author(s)
Year published
2013
Metadata
Show full item recordAbstract
Mobile agent technology offers a number of advantages to resource constrained Wireless Sensor Networks (WSNs) by facilitating parallelism, code and data dissemination, localization, and distributed security services. As part of the second line of defense for WSNs, anomaly detection schemes are also benefiting from mobile agent technology. The formal verification can be used to validate the correctness of a system using formal specifications. This study employs Behavior Trees (BTs) for formal verification of mobile agent based anomaly detection system in WSNs. We employed BT based formal semantics to integrate the behavior ...
View more >Mobile agent technology offers a number of advantages to resource constrained Wireless Sensor Networks (WSNs) by facilitating parallelism, code and data dissemination, localization, and distributed security services. As part of the second line of defense for WSNs, anomaly detection schemes are also benefiting from mobile agent technology. The formal verification can be used to validate the correctness of a system using formal specifications. This study employs Behavior Trees (BTs) for formal verification of mobile agent based anomaly detection system in WSNs. We employed BT based formal semantics to integrate the behavior projection of different components of anomaly detection system. The Symbolic Analysis Laboratory (SAL) tool is used to formally specify the behavior tree model. The analysis based on Linear Temporal Logic (LTL) theorems validates the completeness and consistency of the formal model of mobile agent based anomaly detection system.
View less >
View more >Mobile agent technology offers a number of advantages to resource constrained Wireless Sensor Networks (WSNs) by facilitating parallelism, code and data dissemination, localization, and distributed security services. As part of the second line of defense for WSNs, anomaly detection schemes are also benefiting from mobile agent technology. The formal verification can be used to validate the correctness of a system using formal specifications. This study employs Behavior Trees (BTs) for formal verification of mobile agent based anomaly detection system in WSNs. We employed BT based formal semantics to integrate the behavior projection of different components of anomaly detection system. The Symbolic Analysis Laboratory (SAL) tool is used to formally specify the behavior tree model. The analysis based on Linear Temporal Logic (LTL) theorems validates the completeness and consistency of the formal model of mobile agent based anomaly detection system.
View less >
Conference Title
PROCEEDINGS OF THE 2013 38TH ANNUAL IEEE CONFERENCE ON LOCAL COMPUTER NETWORKS WORKSHOPS (LCN WORKSHOPS)