一种基于问题框架方法的时间需求建模与验证方法

摘要

本发明公开了一种基于问题框架的时间需求建模与验证方法，用于时间攸关系统的时间需求建模与规范的一致性验证，本发明涉及到的操作包括：（1）基于问题框架方法的功能需求模型问题图，借用时钟约束规约语言(CCSL)中的逻辑时钟及时钟关系概念，将交互和问题领域定义为逻辑时钟，利用时钟约束定义待开发时间攸关软件系统交互环境（包括交互和问题领域）的时间约束，包括定量与定性关系，建立时间需求模型，并通过环境的时间约束导出待开发系统的时间规约。（2）定义时钟约束的形式化语义，根据语义建立时钟约束到NuSMV描述的转换规则，利用规则将时间规约转换为NuSMV描述，根据一致性属性的计算树逻辑(CTL)表达式，使用模型检测工具NuSMV来验证时间规约的一致性。