计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2006年
23期
52-57
,共6页
CTL%Petri Net%约束%一致性
CTL%Petri Net%約束%一緻性
CTL%Petri Net%약속%일치성
通过分支时序逻辑(CTL)公式表示系统约束,利用Petri网的可达性分析技术来验证约束一致性是一种重要的、切实可行的约束一致性验证方法.文章描述了一种由CTL公式向Petri网映射的算法,将表示系统约束和组件约束的CTL公式分别映射为Petri网,然后利用Petri网的组合、可达性分析等技术从语义上来验证系统约束与组件约束的一致性.最后,通过对算法的实现开发了一个工具包,并通过一个实例验证了算法正确性和约束一致性验证方法的可行性.
通過分支時序邏輯(CTL)公式錶示繫統約束,利用Petri網的可達性分析技術來驗證約束一緻性是一種重要的、切實可行的約束一緻性驗證方法.文章描述瞭一種由CTL公式嚮Petri網映射的算法,將錶示繫統約束和組件約束的CTL公式分彆映射為Petri網,然後利用Petri網的組閤、可達性分析等技術從語義上來驗證繫統約束與組件約束的一緻性.最後,通過對算法的實現開髮瞭一箇工具包,併通過一箇實例驗證瞭算法正確性和約束一緻性驗證方法的可行性.
통과분지시서라집(CTL)공식표시계통약속,이용Petri망적가체성분석기술래험증약속일치성시일충중요적、절실가행적약속일치성험증방법.문장묘술료일충유CTL공식향Petri망영사적산법,장표시계통약속화조건약속적CTL공식분별영사위Petri망,연후이용Petri망적조합、가체성분석등기술종어의상래험증계통약속여조건약속적일치성.최후,통과대산법적실현개발료일개공구포,병통과일개실례험증료산법정학성화약속일치성험증방법적가행성.
