硅谷
硅穀
규곡
SILICON VALLEY
2010年
23期
178-179
,共2页
状态图%模型检验%Kripke%时态逻辑
狀態圖%模型檢驗%Kripke%時態邏輯
상태도%모형검험%Kripke%시태라집
UML(统一建模语言),是一种可视化的标准建模语言,主要应用于设计和分析阶段.UML模型是否正确反映用户需求成为至关重要的问题.因为状态图能够完整的描述一个系统的行为,所以对UML模型进行检测的主要对象是状态图.提出一种以基于EMC[51(显示模型检验)的模型检测方法SECM(状态图显示模型检验过程).为消除状态图的复杂性,将状态图转化为HA(层次自动机).然后,用Kripke结构对层次自动机进行形式化描述,用时态逻辑描述系统的性质.对状态进行标记,判断每个状态是否满足相应的性质,若不满足给出一个不满足性质的状态序列,从而改进.
UML(統一建模語言),是一種可視化的標準建模語言,主要應用于設計和分析階段.UML模型是否正確反映用戶需求成為至關重要的問題.因為狀態圖能夠完整的描述一箇繫統的行為,所以對UML模型進行檢測的主要對象是狀態圖.提齣一種以基于EMC[51(顯示模型檢驗)的模型檢測方法SECM(狀態圖顯示模型檢驗過程).為消除狀態圖的複雜性,將狀態圖轉化為HA(層次自動機).然後,用Kripke結構對層次自動機進行形式化描述,用時態邏輯描述繫統的性質.對狀態進行標記,判斷每箇狀態是否滿足相應的性質,若不滿足給齣一箇不滿足性質的狀態序列,從而改進.
UML(통일건모어언),시일충가시화적표준건모어언,주요응용우설계화분석계단.UML모형시부정학반영용호수구성위지관중요적문제.인위상태도능구완정적묘술일개계통적행위,소이대UML모형진행검측적주요대상시상태도.제출일충이기우EMC[51(현시모형검험)적모형검측방법SECM(상태도현시모형검험과정).위소제상태도적복잡성,장상태도전화위HA(층차자동궤).연후,용Kripke결구대층차자동궤진행형식화묘술,용시태라집묘술계통적성질.대상태진행표기,판단매개상태시부만족상응적성질,약불만족급출일개불만족성질적상태서렬,종이개진.
