期刊文献+

基于可能性混成自动机的CPS属性验证

Modeling and property verification of CPS based on possibility mixed automaton
下载PDF
导出
摘要 针对环境中存在的不确定性因素对信息物理融合系统(CPS)的影响,提出模型可能性混成自动机,在此基础上给出可能性CPS软件模型属性验证的描述语法和语义以及该模型的可能性动态验证方法。通过验证其可达性和安全性,理论证明和实例分析表明该方法是有效的,可描述不确定环境因素下的CPS系统的验证。 Due to the influence of uncertainty factors cyber-physical systems(CPS)in the environment,the property syntax and semantic of possibility CPS software model based on possibility mixed automaton is given in this paper.Meanwhile,the systematic verification method of possibility CPS model is given.Finally,an example analysis shows this method is valid,and it can describe the verification of CPS on the uncertain environment factors.
作者 陈娜 耿生玲 李永明 薄玮 CHEN Na GENG Shengling LI Yongming BO Wei(School of Computer Science, Qinghai Normal University, Xining 810008, Qinghai ,China Network Information Center School of Computer Science, Shaanxi Normal University, Xi'an 710119, Shaanxi, China Department of Computer and Electronic Information, Shaanxi XueQian Normal University, Xi'an 710100, Shaanxi, China)
出处 《陕西师范大学学报(自然科学版)》 CAS CSCD 北大核心 2016年第5期26-32,共7页 Journal of Shaanxi Normal University:Natural Science Edition
基金 国家自然科学基金(61261047) 青海省自然科学基金(2014-Z-910 2015-ZJ-718) 陕西省自然科学基础研究计划(2016JM6033)
关键词 可能性混成自动机 可能性CPS 动态验证 possibility mixed automation possibility CPS dynamic verification
  • 相关文献

参考文献9

  • 1CLARKE E, GRUMBERG O, PELED D. Mode ehec king[M]. London: The MIT Press, 1999: 1-49.
  • 2DOVIER A, QUINTARELI E. Applying model chec king to solve queries on semistructured data[J]. Com puter Languages: Systems and Structures, 2009, 35 143-172.
  • 3LI L J, LI Y M. Model-checking of linear-time proper-ties in possibilistic kripke structure [C]//Quantitative Logic and Soft Computing, Proceedings of the QL&SC 2012. New York: World Scientific, 2012; 287-294.
  • 4李永明.可能LTL模型检测的两种方法[J].陕西师范大学学报(自然科学版),2014,42(6):21-25. 被引量:18
  • 5LEE E. Cyber physical systems: design challenges [C]// Proceedings of llth IEEE International Symposi- um on Object Oriented Real-Time Distributed Compu- ting(ISORC). Washington D C: IEEE Xplore, 2008: 363-369.
  • 6RAJKUMAR R, INSUP L, LUI S. Cyber-physical sys- tems: the next Computing revolution [C]// Proceedings of 47th Design Automation Conference (DAC). New York: ACM, 2010:731- 736.
  • 7SISTLA A, ZEFRAN M, FENG Y. Runtime monito- ring of stochastic cyber-physical systems with hybrid state [C]//2nd International Conference on Runtime Verification(RV 2011). United States : Springer Verlag, 2012:276-293.
  • 8HENZINGER T. The theory of hybrid automata[C]// Proceedings of the llth Annual IEEE Symposium on Logic in Computer Science(LUCS 96). New Brunswick, N J, 1996: 278-292.
  • 9陈娜,耿生玲,李永明,张胜礼.基于可能性混成自动机的CPS建模方法[J].西安邮电大学学报,2016,21(1):101-105. 被引量:3

二级参考文献19

  • 1Edmund E,Grumberg O,Peled D.Model checking[M].Cambridge:The MIT Press,1999.
  • 2Baier C,Katoen J P.Principles of model checking[M].Cambridge:The MIT Press,2008.
  • 3Chechik M,Devereux B,Gurfinkel A.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(4):371-408.
  • 4Li Yongming,Li Lijun.Model checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
  • 5Li Yongming,Li Yali,Ma Zhanyou.Computation tree logic model checking based on possibility measures[EB/OL].[2014-09-15].http://dx.doi.org/10.1016/j.fss.2014.03.009.
  • 6Li Yongming,Ma Zhanyou.Quantitative computation tree logic model checking based on generalized possibility measures[EB/OL].[2014-09-15].http:∥arxiv.org/abs/1409.6466.
  • 7Kupferman O,Lustig Y.Lattice automata[C]∥Cook B,Podelski A.Proceedings of VMCAI2007,Lecture Notes in Computer Science,Berlin:Springer,2007:199-213.
  • 8LEE E.Cyber physical systems:design challenges[C]//Proceedings of 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing(ISORC),May 5-7,2008,Orlando,F L.Washington,D C:IEEE Xplore,2008:363-369.DOI:10.1109/ISORC.2008.25.
  • 9RAJKUMAR R,INSUP L,LUI S.Cyber-physical systems:the next Computing revolution[C]//Proceedings of 47th Design Automation Conference(DAC),June 13-18,2010,Anaheim,C A.New York:ACM,2010:731-736.
  • 10SISTLA A,ZEFRAN M,FENG Y.Runtime monitoring of stochastic cyber-physical systems with hybrid state[C]//2nd International Conference on Runtime Verification(RV 2011).San Francisco,CA,United states:Springer Verlag,2012:276-293.

共引文献19

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部