Schedulability Analysis of WSAN Applications: Outperformance of A Model Checking Approach

TL;DR

This paper compares analytical and model checking approaches for schedulability analysis of WSAN applications, demonstrating the superior performance of a model checking method in terms of scalability and flexibility.

Contribution

The paper introduces a comparative evaluation of two formal analysis methods for WSAN schedulability, highlighting the advantages of model checking over analytical approaches.

Findings

Model checking outperforms analytical methods in scalability.

Highest data acquisition frequency is computed successfully.

Model checking shows greater flexibility and extensibility.

Abstract

Wireless sensor and actuator networks (WSAN) are real-time systems which demand high degrees of reliability requirements. To ensure this level of reliability, different analysis approaches have been proposed for WSAN applications. Among different alternatives, analytical analysis and model checking are two common approaches which are widely used for the formal analysis of WSAN applications. Analytical approaches apply constraint satisfaction methods, whereas model checking generates explicit states of models and analyze them. In this paper, we compare the two approaches in schedulability analysis of WSAN applications using an application for monitoring and control of civil infrastructures, which is implemented on the Imote2 wireless sensor platform. We show how the highest possible data acquisition frequency for this application is computed while meeting the deadlines, and compare the results of the two approaches as well as their scalability, extensibility, and flexibility.