计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2014年
3期
49-54
,共6页
项重写系统%联锁%Maude语言%安全苛求系统%模型检测
項重寫繫統%聯鎖%Maude語言%安全苛求繫統%模型檢測
항중사계통%련쇄%Maude어언%안전가구계통%모형검측
Term Rewriting System%interlocking system%Maude%safety-critical system%model checking
模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术，对于验证系统的正确性，具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法，采用基于项重写系统原理的Maude工具语言，对铁路联锁系统的站场进行形式化建模，通过其语法和语义定义各类约束和离散事件，构架联锁系统属性和行为。在模型建立的基础上，对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明，基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发，对开发安全苛求系统和模型检测方法的实际应用提供借鉴。
模型檢測方法對安全苛求繫統建模的完整性需要一套嚴謹的方法論與技術，對于驗證繫統的正確性，具有傳統方法無法比擬的優勢。提齣利用項重寫繫統建立安全苛求繫統模型與驗證方法，採用基于項重寫繫統原理的Maude工具語言，對鐵路聯鎖繫統的站場進行形式化建模，通過其語法和語義定義各類約束和離散事件，構架聯鎖繫統屬性和行為。在模型建立的基礎上，對聯鎖站場的靜態屬性和安全屬性進行形式化模型驗證。結果錶明，基于項重寫繫統的模型檢測方法可以較好地應用于實際聯鎖繫統軟件的開髮，對開髮安全苛求繫統和模型檢測方法的實際應用提供藉鑒。
모형검측방법대안전가구계통건모적완정성수요일투엄근적방법론여기술，대우험증계통적정학성，구유전통방법무법비의적우세。제출이용항중사계통건립안전가구계통모형여험증방법，채용기우항중사계통원리적Maude공구어언，대철로련쇄계통적참장진행형식화건모，통과기어법화어의정의각류약속화리산사건，구가련쇄계통속성화행위。재모형건립적기출상，대련쇄참장적정태속성화안전속성진행형식화모형험증。결과표명，기우항중사계통적모형검측방법가이교호지응용우실제련쇄계통연건적개발，대개발안전가구계통화모형검측방법적실제응용제공차감。
Modeling and verification methods require a rigorous methodology and technology for the integrity of the safety-critical system modeling, which have incomparable advantages on the correctness, compared with the traditional methods. This paper proposes a method of using the Term Rewriting System to build the model, and using Maude based on Term Rewriting System to ensure the formal description and verification of interlocking system. With the syntax and semantics of Maude, the specification of various types of constraints and discrete events constitutes the properties and behavior of the interlock system. The safety properties and static properties of interlocking station are validated on the basis of formalized model. The result shows that the modeling and verification methods based on Term Rewriting System can be used for the verification of interlocking systems scalability, and this research provides a good reference for the formal modeling and verification of the safety-critical system.
