权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Verifying Interoperability Requirements in Pervasive Systems

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

基本信息

批准号：
EP/F033567/1
负责人：
Michael Fisher
金额：
$ 55.89万
依托单位：
University of Liverpool
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2008
资助国家：
英国
起止时间：
2008 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FF033567%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系统基础设施）中获得的结果和经验教训。