计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2013年
3期
36-40
,共5页
时序描述逻辑%统一建模语言顺序图%静态语义%动态语义%形式化规约%形式化验证
時序描述邏輯%統一建模語言順序圖%靜態語義%動態語義%形式化規約%形式化驗證
시서묘술라집%통일건모어언순서도%정태어의%동태어의%형식화규약%형식화험증
temporal description logic%Unified Modeling Language(UML) sequence diagram%static semantic%dynamic semantic%formal specification%formal verification
根据统一建模语言(UML)顺序图的时序特征,提出一种基于时序描述逻辑ALCQIUs的UML顺序图形式化方法.研究ALCQIUs时序扩展部分的语法和语义、ALCQIus断言公式集一致性定理,给出ALCQIus断言公式集一致性推理算法,并证明该推理算法的可判定性.以公安报警系统为例,说明基于ALCQIus的UML顺序图形式化规约和形式化验证具备可行性,并且ALCQIus为UML顺序图形式化提供了合理的逻辑基础.
根據統一建模語言(UML)順序圖的時序特徵,提齣一種基于時序描述邏輯ALCQIUs的UML順序圖形式化方法.研究ALCQIUs時序擴展部分的語法和語義、ALCQIus斷言公式集一緻性定理,給齣ALCQIus斷言公式集一緻性推理算法,併證明該推理算法的可判定性.以公安報警繫統為例,說明基于ALCQIus的UML順序圖形式化規約和形式化驗證具備可行性,併且ALCQIus為UML順序圖形式化提供瞭閤理的邏輯基礎.
근거통일건모어언(UML)순서도적시서특정,제출일충기우시서묘술라집ALCQIUs적UML순서도형식화방법.연구ALCQIUs시서확전부분적어법화어의、ALCQIus단언공식집일치성정리,급출ALCQIus단언공식집일치성추리산법,병증명해추리산법적가판정성.이공안보경계통위례,설명기우ALCQIus적UML순서도형식화규약화형식화험증구비가행성,병차ALCQIus위UML순서도형식화제공료합리적라집기출.
