paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Towards programming and verification for activity-oriented smart home systems

迈向面向活动的智能家居系统的编程与验证
ASE Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering2020匹配度 2/10 · 该论文属于智能家居领域的活动导向需求建模与运行时验证,虽涉及程序验证和领域特定语言,但与用户核心关注的静态分析、LLM/Agent 程序分析、浮点程序分析及贝叶斯程序分析均无明显关联。引用 0 inbox
Xuansong Li, Wei Song, Xiangyu Zhang
crossref: 2026-09-12

AI 速览

一句话:提出 Actom 框架,支持活动-传感器映射开发,并在运行时监控时序约束性质,以提升智能家居可靠性与安全性。

智能家居系统日益普及,但其活动导向需求的软件工程仍面临可靠性与安全性挑战。用户在执行活动时往往关注传感器状态,现有工作仅初步支持增量式需求开发,缺乏系统化方法保证由不同开发者构建、运行于复杂环境中的系统满足含时序约束的性质。本文提出 Actom 框架,用于识别活动导向需求并进行运行时验证。Actom 支持开发活动与所需传感器读数之间的映射;运行时接收活动识别结果,依据映射触发执行器以提供活动所需物理条件,并持续监控该映射在活动时间段内是否成立。文中还讨论了评估计划,以展示 Actom 的有效性与效率,最终目标是形成系统化框架,促进活动导向需求开发并监控带时序约束的性质。

问题
智能家居活动导向系统缺乏系统化方法来确保可靠性、安全性,尤其是含时序约束的性质。
方法
提出 Actom 框架,支持活动-传感器映射开发,运行时接收活动识别结果、触发执行器,并持续监控映射在时间段内是否成立。
评估
论文讨论了评估计划,用以展示 Actom 的有效性与效率;最终产物是支持活动导向需求开发与时序性质监控的系统化框架。
原文摘要(Abstract)

Smart home systems are becoming increasingly popular. Software engineering of such systems hence becomes a prominent challenge. In this engineering paradigm, users are often interested in considering sensor states while they are performing various activities. Existing works have proposed initial efforts on incremental development method for activity-oriented requirements. However, there is no systematic way of ensuring reliability and security of such systems which may be developed by various developers and may execute in a complex environment. Some properties, especially those including timing constraints, need to be satisfied. In this paper, we introduce Actom, a framework for identification of activity-oriented requirements and runtime verification. Actom supports the development of the mapping between activities and required sensor readings (activity-sensor mapping). At runtime, Actom receives results of activity recognition and is able to trigger actuators to provide the required physical conditions for the activities, as determined by the activity-sensor mapping. Moreover, Actom continuously monitors whether activity-sensor mapping holds over a time period during the activity. We also discuss the evaluation plan to demonstrate the effectiveness and efficiency of Actom. The end product will be a systematic framework to facilitate the development of activity-oriented requirements and monitor properties with timing constraints to improve reliability and security.

链接与引用

DOI 原文 ·

BibTeX
@inproceedings{paperbot5916,
  title = {Towards programming and verification for activity-oriented smart home systems},
  author = {Xuansong Li and Wei Song and Xiangyu Zhang},
  booktitle = {ASE},
  year = {2020},
  doi = {10.1145/3324884.3418906}
}