-
题名形式化方法B的证明技术
被引量：4
- 1
-
-
作者
鹿蕾
-
机构
鲁东大学
-
出处
《现代电子技术》
2005年第23期126-128,共3页
-
文摘
用形式化方法开发软件是提高软件可靠性和开发效率并实现其自动化的关键。形式化方法B是借助于其辅助工具支持从规约到实现的全过程开发工作。本文介绍了B方法的分层开发与证明过程,针对构造AM以及对他进行精化和实现过程中的类型检查、证明义务进行了重点分析,最后通过具体应用说明了B方法的证明技术在实践中的有效性。
-
关键词
形式化方法
抽象机
广义代换
类型检查
证明义务
-
Keywords
formal method
abstract machine
generalized substitution
type checking
proof obligations
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名形式化方法B的精化
- 2
-
-
作者
高洪江
覃征
鹿蕾
邵利平
-
机构
西安交通大学电子与信息工程学院
鲁东大学图书馆
-
出处
《计算机工程》
CAS
CSCD
北大核心
2007年第9期49-51,共3页
-
基金
国家"973"计划基金资助项目(2004CB719401)
国家自然科学基金资助项目(60542004)
-
文摘
形式化方法B支持从抽象规约到实现的完整的开发过程,用于开发安全关键的软件系统。给出了B方法精化的定义后,介绍了抽象机的精化过程与方法,结合实例分析了仅使用前向精化的普通精化规则的不完整性,通过引入反向精化提供了完备的精化理论,二者联合起来能够证明任何正确的精化。
-
关键词
形式化方法
广义代换
抽象机
前向精化
反向精化
证明义务
-
Keywords
Formal method
Generalized substitution
Abstract machine
Forward refinement
Backward refinement
Proof obligations
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名代换序列研究概况
被引量：15
- 3
-
-
作者
文志英
文志雄
-
机构
武汉大学数学系
-
出处
《数学进展》
CSCD
北大核心
1989年第3期270-293,共24页
-
基金
国家自然科学基金
-
文摘
代换序列的研究可追溯到Thue在1906年的工作,在这一工作中,他引入了一个由代换生成的序列(现称为Thue-Morse序列),研究了它的组合性质,给出了若干非重复序列的例子.大半个世纪以来,人们在各个不同的领域的研究中,从各个不同的角度一再地引入该序列并且不断地加以推广,从而引起了对一般的代换序列的研究.在六十和七十年代,这种研究主要集中在与动力系统和自动机理论的联系及其应用上.八十年代以来。
-
关键词
代换序列
自动机序列
广义代换列
-
分类号
O233
[理学—运筹学与控制论]
-
