本文聚焦安全敏感嵌入式系统的信息流安全验证问题。信息流分析（IFA）是验证机密性与完整性的重要手段，但嵌入式系统天然具有并发性与时间相关性，导致既有 IFA 方法往往陷入两难：要么抽象过于粗糙而精度不足、无法判定非法信息流是否存在，要么保持高精度但分析代价（时间/状态空间）高到难以实用。作者在前期工作基础上提出用“自动抽象精化（automatic abstraction refinement）”来缓解这一矛盾：其核心思想是基于状态之间的依赖关系以及已经检测到的潜在信息泄漏迹象，设计启发式策略来自动选择抽象层级——发现可能泄漏时精化抽象以保留细节，依赖关系简单时则采用更粗的抽象以压缩分析开销。前期方法已利用符号执行精确刻画进程间的数据依赖、控制依赖、时序依赖与事件依赖，并用抽象解释对取值进行符号化表示，但抽象层级必须由人工定义；本文的新贡献正是把这些层级的选择交给精心设计的启发式规则自动完成，目标是在可接受的分析时间内保留足以判定“非法信息流是否可能发生”的信息量。作者针对系统设计语言 SystemC 实现了该方法，并在若干共享总线架构上给出实验结果，验证了方案的可行性。论文属于程序设计语言与软件工程（cs.PL、cs.SE）方向的形式化验证研究，适合从事嵌入式/SoC 设计验证、形式化方法与硬件安全属性验证的研究者与工程师阅读。