基于双格的多值模型的精化关系与对称化简

• 作者: 陈哲 陈娟娟 魏欧 黄志球
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 多值模型检测 精化关系 对称化简
• 年，卷（期）: 2013,（22）
• 所属期刊栏目: 理论研究、研发设计
• 页码范围: 40-45
• 页数: 6页
• 分类号: TP301
• 字数: 6299字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1208-0529

摘要

多值模型是传统布尔模型的扩展。与布尔模型相比，多值模型更适合对包含不确定和不一致信息的软件系统进行建模。为了解决模型检测时的状态爆炸问题，研究了对基于双格的多值模型的对称化简方法。提出了一种新的多值模型的精化关系，证明其保持对μ演算公式的模型检测结果的正确性。定义多值模型的对称化简商结构，证明商结构与原模型之间存在互为精化的关系，因此对μ演算公式的模型检测在二者上可以得到相同的结果。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术学院	183	1755	20.0	33.0
2	魏欧	南京航空航天大学计算机科学与技术学院	31	153	7.0	11.0
3	陈哲	南京航空航天大学计算机科学与技术学院	25	189	7.0	13.0
4	陈娟娟	南京航空航天大学计算机科学与技术学院	3	19	2.0	3.0