Formal Verification in Pervasive Systems: FMIS2009 Workshop Proceedings

需积分: 9 201 浏览量更新于2024-08-01 收藏 200KB PDF 举报

本文档是关于"Formal Verification"的学术论文，主要探讨了在"Perspective Systems"领域中的系统验证方法。该研究是由Mark Ryan教授指导的项目的一部分，着重于协议的验证问题。论文发表在2009年的"Electronic Communications of the EASST"（欧洲应用科学和技术学会电子通讯）第三国际研讨会"Formal Methods for Interactive Systems (FMIS2009)"上，共计15页。会议由Michael Harrison、Mieke Massink担任客座编辑，Tiziana Margaria、Julia Padberg和Gabriele Taentzer担任总编辑。作者包括Myrto Arapinis、Muffy Calder、Louise Denis、Michael Fisher、Philip Gray、Savas Konur、Alice Miller、Eike Ritter、Mark Ryan、Sven Schewe、Chris Unsworth和Rehana Yasmin，他们均来自英国伯明翰大学计算机科学学院，以及利物浦大学的计算机科学部门。论文的通信地址列出了各作者的电子邮件。文章的主题"Towards the Verification of Pervasive Systems"表明，研究关注的是如何在无所不在系统（Pervasive Systems）的设计和实现过程中，利用形式化方法确保系统的正确性、安全性以及互操作性。这种系统通常涉及到多个设备、传感器网络和嵌入式系统之间的无缝协作，因此验证的复杂性显著增加。论文可能探讨了模型检查、形式推理、自动化工具、或特定协议如消息传递安全性等方面的理论和实践方法。通过阅读这篇论文，读者可以期待了解如何将形式化验证技术应用于处理实时、分布式和动态环境中的系统，以及在确保数据隐私、可靠性和性能方面所面临的挑战。同时，它还可能提供了案例研究、评估标准或未来研究方向的讨论，为该领域的进一步发展提供宝贵的洞见。

ECEASST

• autonomous behaviour of agents;

• uncertainty in communications;

• teamwork, collaboration and coordination;

• organisations, norms, societal interactions;

• uncertainty in sensing;

• real-time aspects;

• etc...

In addition, such systems often involve humans within the system which directly affect the sys-

tem’s behaviour.

Current state of the art formal methods appear incapable of coping with the veriﬁcation de-

mand introduced by pervasive systems, primarily because reasoning about such systems requires

considering quantitative, continuous and stochastic behaviour. We also require to prove interac-

tion properties which are quite subtle to express.

2 MATCH overview

MATCH (Mobilising Advanced Technology for Care at Home) is a collaborative research project

focused on technologies for care at home. The overall aim of MATCH is to develop a research

base for advanced technologies in support of social and health care at home. The client users for

MATCH will include older people and people with disabilities of all ages. The goal is to enable

people to manage their health and way of life so that they can continue to live independently in

their own homes for longer.

The main aim of the research in the MATCH project is to integrate a number of home-care

technologies into one system that can be installed into a user’s home. This system will provide

support and assistance where needed by realising a number of goals. Goals may include “Warn

the user if they are doing something dangerous”, “ Call for help if the user has an accident and

needs assistance”, “Inform a medical professional if the user’s health deteriorates”.

This could be implemented as a rule based, event driven pervasive system in which a set of

input components such as: motion detectors, RFID readers, temperature sensors, heart monitors,

and microphones, enable the detection of signiﬁcant events. A set of output components such

as: speakers, GUIs, mobile devices, TVs, lights, and tactile devices, allow the system to interact

with the environment. A set of rules will determine under what circumstances the system should

take action and what action should be taken.

A signiﬁcant factor in whether such a system would be adopted within a home would be the

issue of trust. Therefore, it would be advantageous if properties of the MATCH system could

be veriﬁed. This would then provide support to the claims made by the system developers.

Properties of interest can be categorised as (but not limited to) Security, Safety and/or Usability.

3 / 15 Volume X (2009)

剩余15页未读，继续阅读

「已注销」

粉丝: 0

Formal Verification in Pervasive Systems: FMIS2009 Workshop Pro...

最新资源

Formal Verification in Pervasive Systems: FMIS2009 Workshop Pro...

A Roadmap for Formal Property Verification

data ming papers about location

cvpr2010 papers about motion and tracking_part1

awesome-3dbody-papers:about关于3D身体的真棒论文清单

papers of clifford E. Cummings about state machine

Papers

PAPERS

papers

detection papers

My Papers

最新资源