西安交通大学学报
西安交通大學學報
서안교통대학학보
JOURNAL OF XI'AN JIAOTONG UNIVERSITY
2005年
4期
347-350,355
,共5页
贾晓琳%覃征%何坚%虞凡
賈曉琳%覃徵%何堅%虞凡
가효림%담정%하견%우범
软件体系结构%谓词/变迁网%线性时序逻辑%模型验证
軟件體繫結構%謂詞/變遷網%線性時序邏輯%模型驗證
연건체계결구%위사/변천망%선성시서라집%모형험증
针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(Pr/T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法.首先根据体系结构层次模型扩展Pr/T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质,最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性.所提方法结合了Pr/T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础.
針對軟件體繫結構描述語言在分析、驗證軟件構架動態行為中的不足,採用謂詞/變遷(Pr/T)網為軟件體繫結構動態行為建模,併提齣瞭基于線性時序邏輯的軟件體繫結構動態行為模型驗證方法.首先根據體繫結構層次模型擴展Pr/T網建立體繫結構動態行為模型(DFM)併構造DFM的可達圖,然後使用基于自動機理論的方法來驗證模型的時態邏輯性質,最後通過對一箇電子商務繫統實例的併髮控製機製建模和模型檢測,驗證瞭該方法的有效性.所提方法結閤瞭Pr/T網和線性時序邏輯的優點,為進一步開展軟件體繫結構動態行為的分析、驗證奠定瞭基礎.
침대연건체계결구묘술어언재분석、험증연건구가동태행위중적불족,채용위사/변천(Pr/T)망위연건체계결구동태행위건모,병제출료기우선성시서라집적연건체계결구동태행위모형험증방법.수선근거체계결구층차모형확전Pr/T망건입체계결구동태행위모형(DFM)병구조DFM적가체도,연후사용기우자동궤이론적방법래험증모형적시태라집성질,최후통과대일개전자상무계통실례적병발공제궤제건모화모형검측,험증료해방법적유효성.소제방법결합료Pr/T망화선성시서라집적우점,위진일보개전연건체계결구동태행위적분석、험증전정료기출.
