%0 Journal Article
%T 信息物理融合系统的时间需求一致性分析
%A 尹玲？
%A 陈小红？
%A 刘静？
%J 软件学报
%P 400-418
%D 2014
%R 10.13328/j.cnki.jos.004540
%X 信息物理融合系统(cyber-physicalsystem，简称cps)蕴藏着巨大的潜在应用价值.时间在cps中起到非常重要的作用，应该在需求早期阶段明确.提出了一个基于逻辑时钟的cps时间需求一致性分析框架.首先，构建了cps软件的时间需求概念模型，提供时间需求和功能需求的基本概念，并给出了概念模型的形式化语义；然后，在模型制导下，从cps的交互环境特性和约束中提取出其软件时间需求规约.基于形式化语义，定义了时间需求规约的一致性特性.为了支持形式化验证，将时间需求规约转换成nusmv模型，用ctl公式表述要检测的特性，并使用nusmv工具实施了一致性检测.
%K 信息物理融合系统
%K 需求工程
%K 时间需求建模
%K 一致性检测
%K 形式化验证
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4540&flag=1