论文部分内容阅读
提出一套利用B方法中经典AMN记号表达时态规约的函数结构方案以支持实时软件系统的规约和验证。该方案中，时间类型表示为B方法中系统内部支持的非负整数集合，所有依赖于时间的变量都表示成定义域为时间的全函数。该方案可以方便地表达“过去”、“现在”、“稳定”、“跳变”等时态概念。定义了时间类型、“现在”以及与时间有关的变量的宏操作等抽象机，这些抽象机已经通过B工具的一致性验证。可以在实时系统的B形式化规约中直接使用。