计算机科学 ›› 2017, Vol. 44 ›› Issue (4): 66-71.doi: 10.11896/j.issn.1002-137X.2017.04.014
孙程,邢建春,杨启亮,韩德帅
SUN Cheng, XING Jian-chun, YANG Qi-liang and HAN De-shuai
摘要： 地下建筑工程中的设备系统经常处于静止状态,为保证其在需要时能安全可靠地运行,需对设备进行定期的自动巡检。在自动巡检的过程中,设备自动巡检控制逻辑起到了举足轻重的作用。为了解决复杂的设备自动巡检控制逻辑造成的一系列问题,之前提出了一种层级有限自动机(HFA)的形式化模型,并利用HFA对设备自动巡检控制逻辑实现了行为建模,但并未添加时间属性,也未验证其正确性与可靠性。现提出一种层级时间自动机形式化模型,并利用它对设备自动巡检控制逻辑进行建模,再利用UPPAAL对其进行分析与形式化验证,分别验证其安全性、可达性、活性及时间约束,以此来确保其时效正确性与可靠性。这种建模与形式化验证方法弥补了之前无时间约束的漏洞,有效确保了设备自动巡检控制逻辑的正确性与可靠性。最终,该模型通过了模拟和验证,这充分证明了设备自动巡检控制逻辑是正确可靠的。
| [1] YANG Q L,XING J C,WANG P.Implementation and research of device automatic polling system in protective engineering [J].Protective Engineering,2008,30(4):59-64.(in Chinese) 杨启亮,邢建春,王平.防护工程设备自动巡检系统研究与实现[J].防护工程,2008,0(4):59-64. [2] YANG Q L,XING J C,WANG P,et al.Hierarchical finite automation modeling of device automatic polling logic and its implementation [J].Journal of PLA University of Science and Technology,2009,6(10):528-535.(in Chinese) 杨启亮,邢建春,王平,等.设备自动巡检逻辑的层级有限自动机建模与实现[J].解放军理工大学学报,2009,6(10):528-535. [3] ALUR R,HENZINGER T A.A really temporal logic[J].Journal of the ACM,1989,41(1):164-169. [4] ALUR R,DILL D L.A theory of timed automata[J].Theoretical Computer Science,1994,126(94):183-235. [5] FAL H.Formal Verification of Timed Systems:A Survey andPerspective[J].Proceedings of the IEEE,2004,92(8):1281-1282. [6] BENGTSSON J,WANG Y.Timed automata:Semantics,algorithms and tools[M]∥Desel J,ed.Proc.of the Lectures on Concurrency and Petri Nets:Advances in Petri Nets.Berlin:Sprin-ger-Verlag,2004:87-124. [7] VARDI M Y,WOLPER P.An automata-theoretic approach to automatic program verification[C]∥Proceedings of the First Annual IEEE Symp on Logic in Computer Science Lics,1986:322-331. [8] ALUR R.Timed Automata[M]∥Computer Aided Verification,Springer Berlin Heidelberg,1999:8-22. [9] LARSEN K G,PETTERSSON P,YI W.Uppaal in a nutshell[J].International Journal on Software Tools for Technology Transfer,1997,1(1/2):134-152. [10] BEHRMANN G,DAVID A,LARSEN K G.A tutorial on UPPAAL[M]∥Bernardo M,ed.Proc.of the Formal Methods for the Design of Real-Time Systems.Springer-Verlag,2004:200-236. [11] FERSMAN E,KRCAL P,PETTERSSON P,et al.Task auto-mata:Schedulability,decidability and undecidability[J].Information & Computation,2007,205(8):1149-1172. [12] BRARD B,HADDAD S,SASSOLAS M.Interrupt Timed Au-tomata:verification and expressiveness[J].Formal Methods in System Design,2012,40(1):41-87. [13] FLORIAN M,GAMBLE E,HOLZMANN G.Logic Model Chec- king of Time-Periodic Real-Time Systems[C]∥Infotech@aerospace.2013:1-43. [14] SENN E,LAURENT J,JUIN E,et al.Refining Power Con-sumption Estimations in the Component-based AADL Design Flow[C]∥Forum on Specification,Verification and Design Languages,2008(FDL 2008).IEEE,2008:173-178. [15] GLUCK P R,HOLZMANN G J.Using SPIN model checking for flight software verification[C]∥Aerospace Conference Proceedings,2002.IEEE,2002:105-113. [16] CLARKE E M,ZULIANI P.Statistical Model Checking for Cyber-Physical Systems[C]∥International Conference on Automated Technology for Verification and Analysis.Springer-verlag,2011:1-12. [17] HKAN L,YOUNES S.Ymer:A Statistical Model Checker[M]∥Computer Aided Verification.Springer Berlin Heidelberg,2005:429-433. [18] DE l I D G,WEYNS D.Guaranteeing robustness in a mobile learning Application using formally verified MAPE loops[C]∥Proceedings of the 2013 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS).IEEE Computer Society,2013:83-92. [19] BARTELS B,KLEINE M.A CSP-based framework for thespecification,verification,and implementation of adaptive systems[C]∥Proceedings of the 6th International Symposium on Software Engineering for Adaptive and Self-Managing Systems.ACM,2011:158-167. [20] RAMIREZ A J,CHENG B H C.Verifying and Analyzing Adaptive Logic through UML State Models[C]∥ International Conference on Software Testing,Verification,and Validation.IEEE,2008:529-532. [21] LUCKEY M,THANOS C,GERTH C,et al.Multi-Staged Qua-lity Assurance for Self-Adaptive Systems[C]∥2013 IEEE 7th International Conference on Self-Adaptation and Self-Organizing Systems Workshops.IEEE,2012:111-118. |
| No related articles found! |
|
||
首页