电脑知识与技术
電腦知識與技術
전뇌지식여기술
COMPUTER KNOWLEDGE AND TECHNOLOGY
2008年
35期
2159-2160,2162
,共3页
模型检查%SPIN%PKOMELA%语义
模型檢查%SPIN%PKOMELA%語義
모형검사%SPIN%PKOMELA%어의
模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式.该文从语义角度研究了PROMELA语义引擎问题.首先给出PKOMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PKOMELA语法到抽象对象模型的映射,描述了PROMELA指称语义.
模型檢查工具SPIN的覈心是PROMELA語言,對PROMELA語言執行方式的理解決定所描述繫統模型的行為方式.該文從語義角度研究瞭PROMELA語義引擎問題.首先給齣PKOMELA語法的抽象對象模型形式化定義,然後給齣一箇算法來實現PKOMELA語法到抽象對象模型的映射,描述瞭PROMELA指稱語義.
모형검사공구SPIN적핵심시PROMELA어언,대PROMELA어언집행방식적리해결정소묘술계통모형적행위방식.해문종어의각도연구료PROMELA어의인경문제.수선급출PKOMELA어법적추상대상모형형식화정의,연후급출일개산법래실현PKOMELA어법도추상대상모형적영사,묘술료PROMELA지칭어의.
