制造业自动化
製造業自動化
제조업자동화
MANUFACTURING AUTOMATION
2012年
2期
77-79,84
,共4页
时序描述逻辑%UML状态图%形式化规约%形式化验证
時序描述邏輯%UML狀態圖%形式化規約%形式化驗證
시서묘술라집%UML상태도%형식화규약%형식화험증
本文针对UML状态图具有动态行为和时序特征的特点,提出了一种新的描述逻辑,即时序描述逻辑TDDL(SHOIN(D)).首先给出了TDDL(SHOIN(D))的语法和语义,研究了TDDL( SHOIN(D))的断言公式集一致性推理和动作推理问题,给出了TDDL(SHOIN(D))的断言公式集一致性推理算法,并证明了该推理算法的可判定性；然后给出了动作包含、等价关系的判断方法,并证明了这些方法的可判定性.最后利用TDDL(SHOIN(D))对UML状态图进行了形式化验证.
本文針對UML狀態圖具有動態行為和時序特徵的特點,提齣瞭一種新的描述邏輯,即時序描述邏輯TDDL(SHOIN(D)).首先給齣瞭TDDL(SHOIN(D))的語法和語義,研究瞭TDDL( SHOIN(D))的斷言公式集一緻性推理和動作推理問題,給齣瞭TDDL(SHOIN(D))的斷言公式集一緻性推理算法,併證明瞭該推理算法的可判定性；然後給齣瞭動作包含、等價關繫的判斷方法,併證明瞭這些方法的可判定性.最後利用TDDL(SHOIN(D))對UML狀態圖進行瞭形式化驗證.
본문침대UML상태도구유동태행위화시서특정적특점,제출료일충신적묘술라집,즉시서묘술라집TDDL(SHOIN(D)).수선급출료TDDL(SHOIN(D))적어법화어의,연구료TDDL( SHOIN(D))적단언공식집일치성추리화동작추리문제,급출료TDDL(SHOIN(D))적단언공식집일치성추리산법,병증명료해추리산법적가판정성；연후급출료동작포함、등개관계적판단방법,병증명료저사방법적가판정성.최후이용TDDL(SHOIN(D))대UML상태도진행료형식화험증.
