Verifying Interoperability Requirements in Pervasive Systems

验证普及系统中的互操作性要求

• 批准号: EP/F033540/1
• 负责人: Mark Ryan
• 金额: $ 53.3万
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2008
• 资助国家: 英国
• 起止时间: 2008 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FF033540%2F1
• 关键词: Verifying; Interoperability; Requirements; Pervasive; Systems

The success of pervasive computing depends crucially on the ability to build, maintain and augment interoperable systems: components from different manufacturers built at different times are required to interact to achieve the user's overall goals.Pervasive systems often contain devices which must operate in very different environments and connect together in different ways, e.g., over ad-hoc wireless connections to a variety of systems, and still satisfy all the desired security and performance properties. Our approach to verifying these properties is to identify interoperability requirements for the interaction between the devices and their environment. These requirements introduce also an important layer of abstraction because they allow modularity in the verification process: it suffices to show that each mobile device or fixed component meets the interoperability requirements, and that the interoperability requirements entail the desired high-level properties.We argue that this verification framework makes it possible to adapt and extend techniques (such as model checking and process algebras) which have traditionally been used for verifying properties of small homogeneous systems, to large heterogenous systems. To support this thesis, we will develop techniques to verify properties concerning important aspects of heterogenous systems' security, individual and collective behaviour, performance and privacy. We will use the formal techniques to verify the consequent interoperability requirements, and evaluate their effectiveness through case studies.Note that our focus is on the verification of designs; in particular we focus on the design of basic component behaviours and the protocols which dictate access to them and interaction between them. It is important to note our intention is not to develop pervasive computing systems as such, but rather to draw motivation from, and test our ideas in, a number of planned and existing systems.Three case studies are planned; two are with industrial collaborators. The case studies will be drawn from three layers typical within pervasive systems: application, infrastructure and network. One industrial case study will be a healthcare application. One of its crucial features is the need for the monitoring device to operate in different environments. Hence a careful analysis of the necessary interoperability requirements is mandatory for this application. We will develop and apply our techniques as the system is designed, thus influencing directly the design of the application, motivating our techniques as we develop them, and gaining real life experience of applying our techniques in the field. In addition, our past experience indicates that we will also bring in further case studies, as the project develops. Drawing on the variety of expertise of the members of the consortium, we hope to make a step change in verification technology by developing novel techniques and learning which techniques are most effective in different contexts. The outcomes will directly benefit system designers, and indirectly, end users. They will include techniques applicable to a wide range of application domains, and results and lessons learned from three specific applications including a healthcare data capture system and RFID system infrastructure.

普适计算的成功关键取决于建立、维护和增强可互操作系统的能力：不同制造商在不同时间建立的组件需要相互作用以实现用户的总体目标。普适系统通常包含必须在非常不同的环境中运行并以不同方式连接在一起的设备，例如，通过ad-hoc无线连接到各种系统，并且仍然满足所有期望的安全性和性能属性。我们验证这些属性的方法是确定设备与其环境之间交互的互操作性要求。这些要求还引入了一个重要的抽象层，因为它们允许验证过程中的模块化：足以表明每个移动终端或固定组件满足互操作性要求，并且互操作性要求需要所需的高级别属性。我们认为，这种验证框架使适应和扩展技术成为可能（如模型检查和进程代数），传统上用于验证小型同构系统的属性，大型异构系统。为了支持这一论点，我们将开发技术来验证有关异质系统的安全性，个人和集体行为，性能和隐私的重要方面的属性。我们将使用形式化的技术来验证随之而来的互操作性需求，并通过案例研究来评估其有效性。请注意，我们的重点是设计的验证，特别是我们专注于基本组件行为的设计和协议，这些协议规定了对它们的访问和它们之间的交互。值得注意的是，我们的意图不是开发普适计算系统，而是从一些计划中的和现有的系统中汲取动力，并测试我们的想法。案例研究将从普适系统中的三个典型层：应用程序、基础设施和网络中抽取。一个行业案例研究将是医疗保健应用程序。其关键特征之一是需要监控设备在不同的环境中运行。因此，对必要的互操作性需求的仔细分析对于该应用是强制性的。我们将在设计系统时开发和应用我们的技术，从而直接影响应用程序的设计，在开发技术时激励我们的技术，并获得在该领域应用我们的技术的真实的生活经验。此外，我们过去的经验表明，随着项目的发展，我们还将进行进一步的个案研究。利用该联盟成员的各种专业知识，我们希望通过开发新技术和学习哪些技术在不同情况下最有效，从而在核查技术方面实现一个飞跃。这些成果将直接使系统设计人员受益，并间接使最终用户受益。它们将包括适用于广泛应用领域的技术，以及从三个特定应用中吸取的结果和经验教训，包括医疗数据采集系统和RFID系统基础设施。

项目成果

Verifying Privacy-Type Properties in a Modular Way

• DOI: 10.1109/csf.2012.16
• 发表时间: 2012-06
• 期刊: 2012 IEEE 25th Computer Security Foundations Symposium
• 作者: Myrto Arapinis;Vincent Cheval;S. Delaune

Analysis of privacy in mobile telephony systems

移动电话系统中的隐私分析

• DOI: 10.1007/s10207-016-0338-9
• 发表时间: 2016
• 期刊: International Journal of Information Security
• 影响因子: 3.2
• 作者: Arapinis M

StatVerif: Verification of Stateful Processes

StatVerif：状态进程的验证

• DOI: 10.1109/csf.2011.10
• 发表时间: 2011
• 作者: Arapinis M

Stateful applied pi calculus: Observational equivalence and labelled bisimilarity

有状态应用 pi 演算：观察等价性和标记的双相似性

• DOI: 10.1016/j.jlamp.2017.03.001
• 发表时间: 2017
• 期刊: Journal of Logical and Algebraic Methods in Programming
• 影响因子: 0.9
• 作者: Arapinis M