Formal verification of a pervasive messaging system
Formal verification of a pervasive messaging system
复制标题
DOI：
10.1007/s00165-013-0277-4
复制
发表时间：
2014-07-01
影响因子：
1
通讯作者：
Knox, Stephen
中科院分区：
文献类型：
--
作者：
Konur, Savas;Fisher, Michael;Knox, Stephen
随着普适计算成为现实，其应用越来越多地被用于业务关键、任务关键甚至安全关键领域。这样的系统必须证明有保证的正确性。对系统行为进行详尽分析的一种方法是形式验证，根据所有可能的系统行为对每个重要需求进行逻辑评估。虽然形式验证经常用于安全分析，但很少用于分析部署的普适应用程序。如果没有这种形式，就很难确定系统将根据其输入和环境表现出正确的行为。在本文中，我们将展示如何模型检测技术可以应用于分析的概率行为的普及系统。作为一个案例研究，我们将这种技术应用到现有的普遍的消息转发系统，Scatterbox。散射盒融合了普适系统的许多典型特征，如对传感器可靠性的依赖和对上下文的依赖。我们评估系统的动态时间行为，包括概率元素的分析，使我们能够验证正式的要求，即使在传感器中存在不确定性。我们还得出了一些初步的结论，关于普适计算中使用的形式验证。
As ubiquitous computing becomes a reality, its applications are increasingly being used in business-critical, mission-critical and even in safety-critical, areas. Such systems must demonstrate an assured level of correctness. One approach to the exhaustive analysis of the behaviour of systems is formal verification, whereby each important requirement is logically assessed against all possible system behaviours. While formal verification is often used in safety analysis, it has rarely been used in the analysis of deployed pervasive applications. Without such formality it is difficult to establish that the system will exhibit the correct behaviours in response to its inputs and environment. In this paper, we show how model-checking techniques can be applied to analyse the probabilistic behaviour of pervasive systems. As a case study we apply this technique to an existing pervasive message-forwarding system, Scatterbox. Scatterbox incorporates many typical characteristics of pervasive systems, such as dependence on sensor reliability and dependence on context. We assess the dynamic temporal behaviour of the system, including the analysis of probabilistic elements, allowing us to verify formal requirements even in the presence of uncertainty in sensors. We also draw some tentative conclusions concerning the use of formal verification for pervasive computing in general.