[00298891]一种基于问题框架方法的时间需求建模与验证方法
交易价格：
面议
所属行业：
分析仪器
类型：
发明专利
技术成熟度：
正在研发
专利所属地：中国
专利号：CN201510358917.3
交易方式：
技术转让
技术转让
技术入股
联系人：
华东师范大学
进入空间
所在地：上海上海市
- 服务承诺
- 产权明晰
-
资料保密
对所交付的所有资料进行保密
- 如实描述
技术详细介绍
摘要：本发明公开了一种基于问题框架的时间需求建模与验证方法，用于时间攸关系统的时间需求建模与规范的一致性验证，本发明涉及到的操作包括：（1）基于问题框架方法的功能需求模型问题图，借用时钟约束规约语言(CCSL)中的逻辑时钟及时钟关系概念，将交互和问题领域定义为逻辑时钟，利用时钟约束定义待开发时间攸关软件系统交互环境（包括交互和问题领域）的时间约束，包括定量与定性关系，建立时间需求模型，并通过环境的时间约束导出待开发系统的时间规约。（2）定义时钟约束的形式化语义，根据语义建立时钟约束到NuSMV描述的转换规则，利用规则将时间规约转换为NuSMV描述，根据一致性属性的计算树逻辑(CTL)表达式，使用模型检测工具NuSMV来验证时间规约的一致性。
摘要：本发明公开了一种基于问题框架的时间需求建模与验证方法，用于时间攸关系统的时间需求建模与规范的一致性验证，本发明涉及到的操作包括：（1）基于问题框架方法的功能需求模型问题图，借用时钟约束规约语言(CCSL)中的逻辑时钟及时钟关系概念，将交互和问题领域定义为逻辑时钟，利用时钟约束定义待开发时间攸关软件系统交互环境（包括交互和问题领域）的时间约束，包括定量与定性关系，建立时间需求模型，并通过环境的时间约束导出待开发系统的时间规约。（2）定义时钟约束的形式化语义，根据语义建立时钟约束到NuSMV描述的转换规则，利用规则将时间规约转换为NuSMV描述，根据一致性属性的计算树逻辑(CTL)表达式，使用模型检测工具NuSMV来验证时间规约的一致性。
