Computer Science ›› 2017, Vol. 44 ›› Issue (4): 66-71.doi: 10.11896/j.issn.1002-137X.2017.04.014

Previous Articles     Next Articles

Modeling and Verifying Device Automatic Polling Control Logic Using Hierarchical Timed Automata

SUN Cheng, XING Jian-chun, YANG Qi-liang and HAN De-shuai   

  • Online:2018-11-13 Published:2018-11-13

Abstract: The device systems in the underground construction are often dormant.In order to ensure they can operate securely and reliably when they are needed,it is necessary to poll automatically on the devices at a regular interval.In the automatic polling process,the device automatic polling control logic is of great importance.To solve these problems which are caused by device automatic polling control logic,one formal model of hierarchical finite automaton(HFA) was set up and discussed previously,and modeled for device automatic polling control logic with HFA.But we didn’t add time constraints and verify its accuracy and reliability.This paper proposed a formal model of hierarchical timed automata and modeled with it to the device automatic polling control logic.Then we analyzed and carried out formal verification with UPPAAL to the model.We verified its safety,reachability,activation and time constraint respectively to make sure the accuracy of timeliness and reliability.The method of modeling and formal verification makes up the disadvantage without time constraints in the former and ensures the accuracy and reliability of the device automatic polling control logic effectively.Finally,this model passes the simulation and formal verification,which proves the device automatic polling control logic is correct and reliable.

Key words: Automatic polling,Hierarchical timed automata,UPPAAL,Model checking

[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] BRARD 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] HKAN 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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!