Z规格说明的推理与验证

• 作者: 温晋杰 赵卫华 赵正旭
• 来源期刊: 微型电脑应用
• 学科: 工学
• 关键词: Z规格说明 推理 验证 形式化 条件
• 年，卷（期）: 2016,（11）
• 所属期刊栏目: 基金项目
• 页码范围: 12-16
• 页数: 5页
• 分类号: TP393
• 字数: 3212字
• 语种: 中文

摘要

Z规格说明具有非形式规约不可比拟的严谨性、清晰性.这种描述对于系统内对象的状态描述、行为描述是非常有用的原始参照物.但是,形式化描述不可避免的可能会含有错误或者是矛盾,这些问题在后期必定会导致前期的形式化设计不能付诸实践.因此,有必要做一些形式化的推理与验证来确保Z规约的实施.形式化推理是基于Z规格说明对一个操作模式求其前置条件,即求一个操作成功执行的必要条件,然后对比客观条件是否满足必要条件;形式化验证是一个操作模式求其后置条件,从集合的角度出发验证一个操作成功执行之后所导致的状态量变化是否与操作模式描述一致.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵正旭		52	165	6.0	10.0
2	温晋杰		6	5	2.0	2.0
3	赵卫华		4	2	1.0	1.0