WSAN应用的可调度性分析：模型检测方法之优
网络与互联网体系结构
2022-05-23 v1 形式语言与自动机理论
计算机科学中的逻辑
摘要
无线传感器与执行器网络（WSAN）是具备高可靠性需求的实时系统。为保障此类可靠性，已有多种针对 WSAN 应用的分析方法被提出。在不同方案中，解析分析与模型检查是两种广泛用于 WSAN 应用形式化分析的常见方法。解析方法采用约束满足方法，而模型检查生成模型的显式状态并进行分析。本文中，我们利用一个部署于 Imote2 无线传感器平台、用于土木基础设施监测与控制的应用，比较这两种方法在 WSAN 应用可调度性分析中的表现。我们展示了如何在满足截止时间的前提下计算该应用的最高可能数据采集频率，并比较两种方法的结果及其可扩展性、可扩展性与灵活性。
引用
@article{arxiv.2205.10224,
title = {Schedulability Analysis of WSAN Applications: Outperformance of A Model Checking Approach},
author = {Ehsan Khamespanah and Morteza Mohaqeqi and Mohammad Ashjaei and Marjan Sirjani},
journal= {arXiv preprint arXiv:2205.10224},
year = {2022}
}