计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2004年
11期
1990-1999
,共10页
模型检测%传值进程%带赋值符号迁移图%谓词μ演算%复杂数据结构
模型檢測%傳值進程%帶賦值符號遷移圖%謂詞μ縯算%複雜數據結構
모형검측%전치진정%대부치부호천이도%위사μ연산%복잡수거결구
模型检测是近二十几年来最成功的自动验证技术之一,而模型检测工具的开发是将模型检测和实际相结合的关键.为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻辑公式的语义模型来实现模型检测工具的工作,特别是将复杂数据结构引入传值进程定义语言和带赋值符号迁移图.同时结合实际例子说明模型检测工具的有效性.
模型檢測是近二十幾年來最成功的自動驗證技術之一,而模型檢測工具的開髮是將模型檢測和實際相結閤的關鍵.為瞭有效地對涉及到複雜數據類型的併髮傳值繫統進行模型檢測,總結瞭以擴展的帶賦值符號遷移圖和模態圖分彆作為併髮繫統和邏輯公式的語義模型來實現模型檢測工具的工作,特彆是將複雜數據結構引入傳值進程定義語言和帶賦值符號遷移圖.同時結閤實際例子說明模型檢測工具的有效性.
모형검측시근이십궤년래최성공적자동험증기술지일,이모형검측공구적개발시장모형검측화실제상결합적관건.위료유효지대섭급도복잡수거류형적병발전치계통진행모형검측,총결료이확전적대부치부호천이도화모태도분별작위병발계통화라집공식적어의모형래실현모형검측공구적공작,특별시장복잡수거결구인입전치진정정의어언화대부치부호천이도.동시결합실제례자설명모형검측공구적유효성.
