基于吴方法的多值模型检验

作     者：赵林 吴尽昭 ZHAO Lin;WU Jinzhao

作者机构：北京交通大学轨道交通控制与安全国家重点实验室北京100044 中国科学院成都计算机应用研究所成都610041 

出 版 物：《系统科学与数学》 (Journal of Systems Science and Mathematical Sciences)

年 卷 期：2008年第28卷第8期

页      面：1020-1029页

核心收录：

学科分类：02[经济学] 0202[经济学-应用经济学] 020208[经济学-统计学] 07[理学] 0714[理学-统计学（可授理学、经济学学位）] 070103[理学-概率论与数理统计] 0701[理学-数学] 

基　　金：国家973计划"数学机械化及其在信息技术中的应用"(2004CB318000) "需求工程-对复杂系统的软件工程的基础研究"(2007CB310800) 国家863计划"基于代数符号计算的新型软件形式化验证技术和支持工具"(2007AA01Z143)项目资助 

主　　题：多值模型检验 拟布尔逻辑 多项式 吴方法. 

摘      要：大型复杂系统的开发过程中不可避免的涉及到非确定或不一致信息的处理,而多值模型检验作为经典模型检验的一种扩展,是处理和分析包含此类信息模型的一种有效手段.提出了一种系统化的多值逻辑(涵盖经典逻辑)的代数表示方法,使用吴方法的基本思想和框架实现复杂系统形式验证中基于多值逻辑的模型检验的代数化,建立了通过吴方法实现多值模型检验技术的整体框架.这种代数化的多值模型检验方法可以作为现有方法的有力补充.