科技通报
科技通報
과기통보
BULLETIN OF SCIENCE AND TECHNOLOGY
2011年
2期
186-189,194
,共5页
Petri网%模型验证%调度分析%形式化
Petri網%模型驗證%調度分析%形式化
Petri망%모형험증%조도분석%형식화
针对软件模型的时间约束能力不强以及形式化验证复杂的问题,本文提出一种基于Petri网的形式化模型调度方法,从时间层次上对模型的合理性进行验证与分析.该方法通过构建系统领域模型到Petri网模型的转换规则,利用Petri网的分析验证技术,实现对软件模型的正确性验证,解决了系统建模时存在的问题.应用实例和实验结果验证了该方法的有效性和可行性.
針對軟件模型的時間約束能力不彊以及形式化驗證複雜的問題,本文提齣一種基于Petri網的形式化模型調度方法,從時間層次上對模型的閤理性進行驗證與分析.該方法通過構建繫統領域模型到Petri網模型的轉換規則,利用Petri網的分析驗證技術,實現對軟件模型的正確性驗證,解決瞭繫統建模時存在的問題.應用實例和實驗結果驗證瞭該方法的有效性和可行性.
침대연건모형적시간약속능력불강이급형식화험증복잡적문제,본문제출일충기우Petri망적형식화모형조도방법,종시간층차상대모형적합이성진행험증여분석.해방법통과구건계통영역모형도Petri망모형적전환규칙,이용Petri망적분석험증기술,실현대연건모형적정학성험증,해결료계통건모시존재적문제.응용실례화실험결과험증료해방법적유효성화가행성.