一句话：提出 IoT-LySa 进程演算及静态分析，追踪 IoT 数据来源、聚合与流动，以支持安全等非功能性质验证。
IoT 为信息社会提供基础设施，其中智能对象自动收集并交换来自传感器或聚合生成的数据。为设计并推理此类系统，论文从基础层面研究协调原语与分析机制，提出 IoT-LySa：一种带有静态分析的进程演算。该分析追踪 IoT 数据的来源、被如何操作以及如何在系统中流动，从而刻画数据收集与聚合的路径。其结果可供设计者检查智能对象的行为，特别是验证安全性等非功能性质。摘要未报告具体实现或实验评估，贡献主要在形式化模型与分析机制。
The Internet of Things (IoT) offers the infrastructure of the information society. It hosts smart objects that automatically collect and exchange data of various kinds, directly gathered from sensors or generated by aggregations. Suitable coordination primitives and analysis mechanisms are in order to design and reason about IoT systems, and to intercept the implied technological shifts. We address these issues from a foundational point of view. To study them, we define IoT-LySa, a process calculus endowed with a static analysis that tracks the provenance and the manipulation of IoT data, and how they flow in the system. The results of the analysis can be used by a designer to check the behaviour of smart objects, in particular to verify non-functional properties, among which security.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BodeiDFG16a,
title = {Tracing where IoT data are collected and aggregated},
author = {Chiara Bodei and Pierpaolo Degano and Gian-Luigi Ferrari and Letterio Galletta},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:5)2017}
}