基于Event-B的列车车载控制器系统的形式化建模
被引量：1
摘要
介绍了列车车载控制器系统(Vehicle On-borad controller system)的系统结构和功能,采用Event-B建模理论对VOBC的系统结构与功能模式做了建模所必要的功能(FUN)列表定义与环境规约(EV)分类描述,给出了基于Event-B方法的VOBC执行指令的建模流程并指出了模型的分层提精步骤,对最终建立好模型进行了验证。
出处
《数字技术与应用》
2012年第8期13-13,共1页
Digital Technology & Application
参考文献2
-
1J.R.Abrial.Modeling in Event-B:System and Software Engineering.Cambridge UniversityPress 2010.
-
2Haugen E G.Probabilistic MechanicaIDesign[M].New York:Wiley, 1980.
同被引文献12
-
1Abrial J R.Modeling in Event-B:System and software engineering[M].Cambridge:Cambridge University Press,2010.
-
2Abrial J R,Su W,Zhu H.Formalizing hybrid systems with Event-B[C]∥Proc of the 3rd International Conference on Abstract State Machines,2012:178-193.
-
3Damchoom K,Butler M,Abrial J R.Modelling and proof of a tree-structured file system in Event-B and Rodin[C]∥Proc of the 10th International Conference on Formal Engineering Methods,2008:25-44.
-
4Shi J,Zhu L,Fang H,et al.xBIL--A hardware resource oriented binary intermediate language[C]∥Proc of 2012 17th International Conference on Engineering of Complex Computer Systems(ICECCS’12),2012:211-219.
-
5Shi J,He J,Zhu H,et al.ORIENTAIS:Formal verified OSEK/VDX real-time operating system[C]∥Proc of 201217th International Conference on Engineering of Complex Computer Systems(ICECCS’12),2012:293-301.
-
6Shi J,Zhu L,Huang Y,et al.Binary code level verification for interrupt safety properties of real-time operating system[C]∥Proc of 2012 6th International Symposium on Theoretical Aspects of Software Engineering(TASE’12),2012:223-226.
-
7Yin L,Mallet F,Liu J.Verification of MARTE/CCSL time requirements in Promela/SPIN[C]∥Proc of 2011 16th International Conference on Engineering of Complex Computer Systems(ICECCS’11),2011:65-74.
-
8Su W,Yang F,Wu X,et al.Formal approaches to mode conversion and positioning for vehicle system[C]∥Proc of2011IEEE 35th Annual Conference Workshops on Computer Software and Applications(COMPSACW’11),2011:416-421.
-
9Stepney S,Cooper D,Woodcock J.An electronic purse:Specification,refinement and proof[R].Technical monograph PRG-126,Oxford:Oxford University Computing Laboratory,2000.
-
10Event-B[EB/OL].[2013-04-20].http:∥www.event-b.org.
-
1琼-雷蒙德·阿布里亚尔.Event—B语言的建模[J].国外科技新书评介,2011(2):15-16.
-
2辛未,穆建成,马连川,曹源.基于Event-B的双机热备平台测试序列自动生成方法[J].铁路计算机应用,2016,25(11):36-40.
-
3谭彦亮,杨桦,乔磊.基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证[J].空间控制技术与应用,2014,40(4):57-62. 被引量：4
-
4吴劲,陈志慧.基于Event-B的形式化建模关键技术研究[J].电子科技大学学报,2014,43(3):405-408. 被引量：4
-
5定制WindowsXP位置栏[J].个人电脑,2004,10(4):234-234.
-
6超级解露的剧情快照[J].电脑爱好者（普及版）,2011(A01):92-92.
-
7唐晨,陈邦兴,陈祖希,沈啸.基于Event-B的控制系统形式化建模方法研究[J].佳木斯大学学报（自然科学版）,2014,32(1):33-36.
-
8朱海鹰,陈邦兴,祝玉军.基于MAS的VOBC仿真测试系统研究与设计[J].佳木斯大学学报（自然科学版）,2014,32(6):859-862.
-
9章玥,郭建,朱晓冉,王文君,朱晶洋,汤家华,陈峻念.基于Event-B方法的多应用智能卡的建模与开发[J].计算机工程与科学,2014,36(10):1943-1951. 被引量：2
-
10赵大勇.基于智能优化控制的磨矿过程综合自动化系统[J].自动化信息,2008(10):67-69.
