论文标题
WSAN应用程序的可调度性分析：模型检查方法的表现超出
Schedulability Analysis of WSAN Applications: Outperformance of A Model Checking Approach
论文作者
论文摘要
无线传感器和执行器网络（WSAN）是需要高度可靠性要求的实时系统。为了确保这种可靠性，已经提出了针对WSAN应用的不同分析方法。在不同的替代方案中，分析分析和模型检查是两种常用方法，这些方法被广泛用于WSAN应用的形式分析。分析方法采用约束满意度方法，而模型检查产生了模型的明确状态并分析它们。在本文中，我们使用用于监视和控制民用基础架构的应用程序对WSAN应用程序进行计划分析的两种方法，该应用程序在IMOTE2无线传感器平台上实现。我们展示了如何在完成截止日期时计算此应用程序的最高数据采集频率，并比较两种方法的结果以及它们的可扩展性，可扩展性和灵活性。
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.
