软件学报:jos:4540 · 记录 #1
信息物理融合系统(cyber-physical system，简称CPS)蕴藏着巨大的潜在应用价值.时间在CPS中起到非常重要的作用，应该在需求早期阶段明确.提出了一个基于逻辑时钟的CPS时间需求一致性分析框架.首先，构建了CPS软件的时间需求概念模型，提供时间需求和功能需求的基本概念，并给出了概念模型的形式化语义；然后，在模型制导下，从CPS的交互环境特性和约束中提取出其软件时间需求规约.基于形式化语义，定义了时间需求规约的一致性特性.为了支持形式化验证，将时间需求规约转换成NuSMV模型，用CTL公式表述要检测的特性，并使用NuSMV工具实施了一致性检测.
这些页面提供论文线索，不代表同行评审或质量认证。
此版本尚未生成 AI 解读。解读由后台任务生成并按论文版本保存，登录后共享已有结果。
2014 · 正式发表 · DOI: 10.13328/j.cnki.jos.004540
目前只观测到一个版本，无法比较变化。之后收录新版本时，会在这里对照标题、作者、分类和摘要。
平台记录号代表本站观测到的元数据变化，不是作者修订号。来源日期仅到月份或年份时，按该月或该年首日存档。
信息物理融合系统(cyber-physical system，简称CPS)蕴藏着巨大的潜在应用价值.时间在CPS中起到非常重要的作用，应该在需求早期阶段明确.提出了一个基于逻辑时钟的CPS时间需求一致性分析框架.首先，构建了CPS软件的时间需求概念模型，提供时间需求和功能需求的基本概念，并给出了概念模型的形式化语义；然后，在模型制导下，从CPS的交互环境特性和约束中提取出其软件时间需求规约.基于形式化语义，定义了时间需求规约的一致性特性.为了支持形式化验证，将时间需求规约转换成NuSMV模型，用CTL公式表述要检测的特性，并使用NuSMV工具实施了一致性检测.
查看此版本解读 →查看此版本原文 ↗