💻 computer science

A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes

本文提出了一种个性化形式化验证框架，该框架将传感器数据与个体情境相结合，通过使用线性时序逻辑来检测安全违规并生成解释性反例，从而对独立生活的老年人的日常生活活动进行建模与形式化验证。

原作者： Ricardo Contreras, Filip Smola, Nuša Farič, Jiawei Zheng, Jane Hillston, Jacques D. Fleuriot

发布于 2026-01-15

📖 1 分钟阅读☕ 轻松阅读

原作者： Ricardo Contreras, Filip Smola, Nuša Farič, Jiawei Zheng, Jane Hillston, Jacques D. Fleuriot

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你有一个非常聪明、非常有耐心的数字助手，陪伴在一位老年人身边。这个助手不仅仅是在观察，它还试图理解这个人的独特生活节奏、偏好以及家居布局。你分享的这篇论文描述了一个构建这种助手的全新“规则手册”，它结合了现实世界的传感器和形式逻辑，以确保人们在独立生活的同时既安全又快乐。

以下是该框架的工作原理，通过简单的概念进行了解：

1. 设定：构建数字孪生

把这位老年人的家想象成一个复杂的拼图。为了理解这些拼图块是如何组合在一起的，研究人员并没有仅仅把传感器贴在墙上；他们首先进行了一次深入交谈（半结构化访谈）。

访谈： 他们询问了当事人关于他们的日常习惯、喜好以及不喜欢的事情（比如卧室里的隐私问题）以及他们的活动路径。
传感器： 他们安装了隐蔽的“数字眼睛”（运动传感器）和“数字触觉传感器”（安装在门、抽屉和冰箱上的接触传感器）。这些传感器充当了房屋的神经系统，每当门被打开或有人走过时，它们都会发出微小的信号。
结果： 他们将访谈笔记与传感器数据相结合，构建了一个个性化数字孪生体。这不是一个通用的模型，而是为那个特定的人量身定制的、关于其生活与家居的专属地图。

2. 规则手册：编写“如果-那么”的故事

一旦拥有了数字孪生体，他们就需要一种方法来检查这个人是否正在做他们通常会做的事情。他们没有直接观察原始数据，而是使用了一种叫做线性时序逻辑 (LPL) 的特殊语言编写了“规则手册”。

这就像是在编写一个具有严格情节点的故事。

示例规则 1（晨间淋浴）： “一旦当事人从卧室醒来并离开卧室，他们必须最终前往走廊，然后进入浴室，最后关闭淋浴门。”
示例规则 2（宠物食物）： “如果在早晨打开了冰箱，这必须发生在打开任何厨房橱柜之前。”（这是针对一位参与者的特定偏好，他在吃早餐前先喂宠物）。
示例规则 3（药物）： “要拿到药物，当事人必须先经过客厅。”

这些规则是用一种精确的数学语言编写的，计算机可以阅读且不会产生歧义。

3. 裁判：模型检测器

这就是见证奇迹的地方。研究人员使用了一个名为 NuSMV 的工具，它扮演着一个超快、不知疲倦的“裁判”角色。

裁判获取数字孪生体（房屋和传感器的地图）和规则手册（LPL 规则）。
它像查看电影胶片一样运行一整天的所有数据，逐一检查每一幕是否符合规则。
如果遵守了规则： 裁判会说：“一切正常！”
如果违反了规则： 它不会只打印出“错误”，而是会打印出一个反例 (Counter-Example)。这就像是一个“回放”，展示了故事在何处偏离了剧本。

4. 他们的发现（结果）

团队在两个不同的参与者（我们称之为参与者 A 和参与者 B）身上测试了该系统，以观察其效果。

“差一点”的失误： 对于参与者 A，规则是：“卧室 -> 走廊 -> 浴室 -> 淋浴门关闭”。在某天早上，此人的路径是：卧室 -> 走廊 -> 浴室 -> 走廊 -> 浴室 -> 关闭淋浴门。
- 计算机将其标记为“违规”，因为此人又回到了走廊。
- 洞察： 此人确实洗了澡，但他们的流程中出现了一个微小的绕路。系统捕捉到了这一点，表明规则可能需要稍微增加一些灵活性，以允许一些无害的小变动。
“遗漏”的步骤： 对于参与者 B，规则是关于服药的。规则规定他们必须经过客厅才能拿到药物。在某一天，此人在预定时间窗口之后才经过客厅。
- 洞察： 系统将其标记为违规。这很重要，因为与洗澡不同，错过预定的服药时间可能会带来安全风险。系统成功识别出：该活动虽然发生了，但发生的时间不对。

5. 核心结论

该论文声称，这一框架是监测老年人的强大新方法。它不仅仅是在监视他们，更是在理解他们的特定语境。

它是个性化的： 它尊重隐私（不使用摄像头），并能适应每个人的特定家居环境和习惯。
它是精确的： 它利用数学来证明某种行为对于该特定个人而言是“安全”或“正常”的。
它是一个安全网： 它可以识别出人们何时偏离了常规，无论是无害的变化（如洗澡晚了几分钟），还是潜在的警告信号（如忘记服药）。

研究人员得出结论，虽然该系统运作良好，但人类的行为是复杂多变的。有时传感器看到冰箱被打开，但我们并不知道是否真的吃了东西。然而，通过将传感器与个人的故事和偏好相结合，这个框架比以往任何时候都更清晰、更个性化地描绘了他们的日常生活图景。

技术摘要：一种用于日常生活活动监测的个性化形式化验证框架

问题陈述
本文针对日益增长的独立生活老年人（OAs）在提升生活质量（QoL）和保障安全方面的紧迫需求进行了研究。虽然基于传感器的日常生活活动（ADLs）监测在检测健康下降方面已趋于成熟，但现有方法往往缺乏个性化。许多系统依赖于对常规行为和位置的通用假设，未能考虑到个人的偏好、特定的家居布局以及隐私顾虑。此外，以往利用形式化方法进行 ADL 监测的工作大多局限于受控的模拟环境，而非真实的居家环境。核心挑战在于开发一种系统，能够严谨地验证观察到的个体行为是否符合其特定的安全与常规要求，同时避免强加“一刀切”的模型。

方法论
作者提出了一种将无感商业传感器数据与通过半结构化访谈及社会学观察获得的丰富上下文信息相结合的框架。该方法论通过以下阶段进行：

数据收集：
- 定性研究： 研究人员通过半结构化访谈来绘制日常规律、偏好、隐私边界和特定需求。这为传感器布置和属性定义提供了依据。
- 定量研究： 在参与者的家中部署接触式传感器（监测门、抽屉、家电）和被动红外（PIR）运动传感器。数据通过 Home Assistant 进行聚合并存储在 InfluxDB 中。
- 参与者： 研究对象为 10 名居住在苏格兰爱丁堡的老年人（年龄 67–97 岁）。论文详细展示了两位具有不同常规行为的参与者（A 和 B）的案例研究。
数据预处理：
- 对传感器数据进行清洗，以去除噪声（例如接触式传感器的温度波动）和冗余的状态更新。
- 运动传感器事件被视为瞬时转换，除非是标记运动序列结束，否则移除“清除（clear）”状态。
- 数据被分割成带有 10 分钟重叠的 20 分钟“子轨迹（subtraces）”，以应对模型检测中固有的状态空间爆炸问题。
形式化建模：
- 模型生成： 一个自动化工具根据参与者的房屋布局（表示为房间的有向图）和特定的传感器配置生成有限状态转换系统（使用 NuSMV）。
- 状态表示： 模型追踪传感器状态（开启/关闭、检测到/清除）以及参与者在房间之间的移动。
- 属性规范： 要求被编码为过去线性时间逻辑（pLTL），这是包含过去时间算子的线性时间逻辑（LTL）的扩展。这使得能够相对于当前时间对事件序列进行推理。属性源自访谈分析，并分为通用类（如卫生）、个人特定类（如宠物护理）或基于常规类（如药物服用）。
验证：
- NuSMV 模型检查器验证生成的模型是否满足 pLTL 属性。
- 如果某个属性被违反，NuSMV 会生成反例（一个特定的状态序列）以识别偏差的原因。

主要贡献
论文概述了三个主要贡献：

一个综合框架： 它将形式化模型验证与商业传感器数据以及显性的上下文信息（访谈、房屋布局、观察）相结合，以创建个性化模型。这实现了将传感器事件直接与个人偏好和需求相联系。
系统化的规范方法： 它提供了一种从半结构化访谈中推导形式化属性的严谨方法，确保验证标准反映了每位参与者的独特背景。
现实世界环境中的泛化能力： 该框架在两个具有不同 ADLs 的不同参与者身上得到了验证，证明了其在受控实验室环境之外的多种生活情况和常规行为中的适应性。

结果与分析
该框架被用于验证两名参与者的特定晨间常规：

参与者 A： 验证的属性包括特定的洗澡序列（卧室 $\to$ $\to$ 走廊 $\to$ $\to$ 浴室 $\to$ $\to$ 淋浴门关闭）以及特定的喂养宠物序列（在打开其他橱柜之前先打开冰箱）。
- 发现： 洗澡属性在大多数日子里得到满足，但由于一次微小的偏差（在关闭淋浴门之前返回了走廊）而发生违反。宠物喂养属性在周日被违反了一次，这可能是由于周末常规的变化所致。
参与者 B： 验证了一个属性，即从客厅移动到厨房以获取药物分配器的序列。
- 发现： 该属性在大多数日子里得到满足，但在一个周五被违反，当时参与者在定义的窗口时间之后（上午 9:50 而非 7:00–9:00 窗口）使用了药物。

分析强调，虽然框架能够成功识别偏差，但一些“违反”源于轻微的、非关键性的常规转变（例如稍晚一点或以不同的顺序洗澡），而非安全风险。相反，在预定时间服用药物的偏差则被标记为潜在的安全风险。研究还指出了局限性，包括传感器故障（约 1% 的数据）、来自宠物/访客的噪声，以及传感器事件固有的歧义性（例如，打开冰箱并不保证一定消耗了食物）。

意义与主张
论文声称，该框架提供了一种全新的、以人为本的 ADL 监测方法，超越了通用的健康警报。通过结合形式化验证与定性上下文，该系统可以：

随着时间的推移检测非预期的行为。
区分常规偏差与潜在的安全风险。
当关键属性（如服药依从性）被违反时，提供及时干预的机制。

作者保持了审慎的态度，承认虽然该框架在增强安全性和福祉方面展现出潜力，但在理解传感器数据和人类行为的多变性方面仍面临挑战。他们得出结论，该方法在现实世界部署中是可行的，但需要对时间要求进行仔细优化，以适应日常生活的自然灵活性。