基于形式语言B的一种新的时态规约方案  

A New Scheme of Temporal Specification in B Language

作　　者：肖健宇[1] 张德运[1] 陈海诠[1] 董皓[1] 

机构地区：[1]西安交通大学电子与信息工程学院

出　　处：《微电子学与计算机》2006年第2期16-19,共4页Microelectronics & Computer

基　　金：国家863计划项目(8633010503)

摘　　要：提出一套利用B方法中经典AMN记号表达时态规约的函数结构方案以支持实时软件系统的规约和验证。该方案中,时间类型表示为B方法中系统内部支持的非负整数集合,所有依赖于时间的变量都表示成定义域为时间的全函数。该方案可以方便地表达“过去”、“现在”、“稳定”、“跳变”等时态概念。定义了时间类型、“现在”以及与时间有关的变量的宏操作等抽象机,这些抽象机已经通过B工具的一致性验证,可以在实时系统的B形式化规约中直接使用。A scheme of temporal specification using function construct of classical B AMN is proposed to support specification and verification of real-time software system. In this scheme, the time related specification can be expressed and verified in the currently existed B tools without any extensions. Time type is represented by B＇s non-positive integer. The start point of time memorized hy a constant is determined by the expression of the longest peroid of time in the specified system. In the initialization of the specification,‘Now＇ is set to be a value equal to or larger than the maximum period. All the time dependent variables are represented by a total function with the domain of time. This method can easily express the temporal concept of ＂previous＂, ＂now＂, ＂stable＂ and ＂edge＂ etc. Abstract machines of time type, ＂now＂ and operation macros of signal （time-related variables） are defined which have been verified by the B tool and can be used directly in the B formal specification of real-time systems.

关 键 词：时态规约 形式化方法 实时系统 B方法 B函数 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]