信息物理融合系统的时间需求一致性分析

• 作者: 刘静 尹玲 陈小红
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 信息物理融合系统 需求工程 时间需求建模 一致性检测 形式化验证
• 年，卷（期）: 2014,（2）
• 所属期刊栏目: 嵌入式系统软件设计方法与技术专刊
• 页码范围: 400-418
• 页数: 19页
• 分类号: TP311
• 字数: 13564字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004540

摘要

信息物理融合系统(cyber-physical system,简称CPS)蕴藏着巨大的潜在应用价值.时间在CPS中起到非常重要的作用,应该在需求早期阶段明确.提出了一个基于逻辑时钟的CPS时间需求一致性分析框架.首先,构建了CPS软件的时间需求概念模型,提供时间需求和功能需求的基本概念,并给出了概念模型的形式化语义;然后,在模型制导下,从CPS的交互环境特性和约束中提取出其软件时间需求规约.基于形式化语义,定义了时间需求规约的一致性特性.为了支持形式化验证,将时间需求规约转换成NuSMV模型,用CTL公式表述要检测的特性,并使用NuSMV工具实施了一致性检测.