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.

普遍计算的成功取决于构建，维护和增强可互操作系统的能力：在不同时间构建的不同制造商的组件需要进行交互以实现用户的整体目标，通常包含在非常不同的环境中运行的设备，并且必须在不同的环境中运行，并以不同的方式连接到不同的无线连接，以达到无线连接，以使各种系统不满意和各种系统，并且各种各样的效率以及各种各样的各种效率和各种各样的各种效率和各种各样的各种各样的效率和各种各样的效率。我们验证这些属性的方法是确定设备与其环境之间相互作用的互操作性要求。这些要求还引入了重要的抽象层，因为它们允许在验证过程中模块化：足以表明每个移动设备或固定组件都满足互操作性的要求，并且互操作性要求需要所需的高级属性。我们认为，此验证框架可以适应和扩展验证技术（例如模型范围）的验证框架（诸如型号的验证）（诸如型号）的范围（诸如验证）的范围（诸如型号）。系统，大型异源系统。为了支持这一论点，我们将开发技术来验证有关异源系统安全，个人和集体行为，绩效和隐私的重要方面的属性。我们将使用正式技术来验证随之而来的互操作性要求，并通过案例研究评估其有效性。注意我们的重点是设计验证；特别是，我们专注于基本组件行为的设计以及决定访问它们的协议以及它们之间的相互作用。重要的是要注意，我们的意图是不开发普遍的计算系统，而是要从计划和现有的系统中汲取动力并测试我们的想法。计划进行三个案例研究；有两个与工业合作者在一起。案例研究将来自普遍系统中典型的三层：应用，基础架构和网络。一个工业案例研究将是医疗保健。它的关键特征之一是需要监视设备在不同的环境中操作。因此，对于此应用，必须仔细分析必要的互操作性要求。当系统的设计时，我们将开发和应用我们的技术，从而直接影响应用程序的设计，在开发它们时激发我们的技术，并获得现实生活中的经验，以将我们的技术应用于现场。此外，我们过去的经验表明，随着项目的发展，我们还将引入进一步的案例研究。利用财团成员的各种专业知识，我们希望通过开发新颖的技术和学习哪些技术在不同情况下最有效的技术来改变验证技术的步骤。结果将直接使系统设计师和最终用户间接受益。它们将包括适用于广泛应用领域的技术，以及从包括医疗保健数据捕获系统和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

Privacy through Pseudonymity in Mobile Telephony Systems

• DOI: 10.14722/ndss.2014.23082
• 发表时间: 2014-01-01
• 期刊: 21ST ANNUAL NETWORK AND DISTRIBUTED SYSTEM SECURITY SYMPOSIUM (NDSS 2014)
• 作者: Arapinis, Myrto;Mancini, Loretta Ilaria;Ryan, Mark
• 通讯作者: Ryan, Mark

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