期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

SPARDL模型的Event-B解释 被引量：2

Event-B interpretation for space aircraft description language model
下载PDF
导出
摘要 针对由周期行为和模式转换机制组成的实时系统提出的SPARDL需求建模语言,详细阐明了其对应的SPARDL模型的Event-B解释。通过Event-B来解释SPARDL的语义,同时提出一种基于SPARDL模型特征的精化框架用于Event-B模型的开发。最后,通过案例研究的分析展示用Event-B对SPARDL模型建模和验证的方法的有效性。 A requirement modeling language called SPARDL was proposed for modeling and analyzing such periodic control systems consisting of periodic behaviors together with the mode transition mechanism.The Event-B interpretation was specified for the SPARDL model.The semantics of SPARDL were presented by Event-B and a refinement framework was introduced to develop the Event-B models based on the features of the SPARDL model.Finally,a case study was analyzed to show the effectiveness of our proposed approach to modeling and validation of the SPARDL model by Event-B.
作者 綦艳霞 沈慧丽 陈朝晖 顾斌
机构地区 北京控制工程研究所 华东师范大学软件学院
出处 《计算机应用》 CSCD 北大核心 2012年第12期3525-3528,3539,共5页 journal of Computer Applications
基金 国家自然科学基金资助项目(90818024 91118007)
关键词 需求建模语言 周期性控制系统 EVENT-B 需求分析 精化 验证 requirement modeling language periodic control system Event-B requirement analysis refinement verification
分类号 TP311.521 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献12

  • 1WANG ZHENG, LI JIANWEN, ZHAO YONGXIN, et al. SF ARDL: a requirement modeling language for periodic contwl systel I CII/ ISoLA'10: Proceedings of tile 5th International Symposim on Leveraging Applications of Formal Methods, Verification an Validation. Berlin: Springer, 2010:594-608.
  • 2CIMATI'I A, CLARKE E, GIUNCHIGLIA F, et al. NUSMV: a new symbolic model checker[ J]. International Journal on Software "Fools for Technology Transfer, 2000, 2(4) : 2000.
  • 3CLARKE E M, JR GRUMBERG O, PELED D A. Model checking [M]. Cambridge, Massachusetts: MIT Press, 1999.
  • 4HOLZMANN G J. The model checker SPIN[ J]. 1EEE Transactions on Software Engineering, 1997, 23(5) : 279 -295.
  • 5BENGTSSON J, LARSEN K G, LARSSON F, et al. UPPAAI, in 1995[ C]// Proceedings ff the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems. Lon- don: Springer-Verlag, 1996:431 -434.
  • 6BALL T, RAJAMANI S K. The SLAM project: debugging system software via static analysis[ C]// Proceedings of the 29th ACM SIG- PLAN-SIGACT Symposium on Principles of Programming Langua- ges. New York: ACM, 2002: I -3.
  • 7BEYER D, HENZ1NGER T A, JHALA R, et al. The software mod- el checker blast: applications to software engineering[ J]. Interna- tional Journal on Software Tools for Technology Transfer, 2007, 9 (2) : 505 -525.
  • 8CLARKE E, KROENING D, FLAVIO L. A tool for checking ANSI- C programs[ C]//TACAS'94: Tools and Algorithms for the Construc- tion and Analysis of Systems. London: Springer-Verlag, 2004:168 - 17.
  • 9HENZINGER T A, HOROWITZ B, KIRSCH C M. Giotto: a time- triggcred language for embedded programming[ C]// EMSOI'I"OI: Proceedings of the 1st International Workshop on Embedded Soft- ware. London: Springer-Verlag, 2001: 166- 184.
  • 10ABRIAL J R, BUTLER M J, HALLERSTEDE S, et al. Rodin: an open toolset for modelling and reasoning in Event-B[ J]. Internation- al Journal on Software Tools for Technology Transfer, 2010, 12(6) : 447 - 466.

同被引文献24

  • 1RAGHURAJ S, DIVAKAR Y. Modeling of muhiversion concurrencycontrol system using Event-B [ C]//Proceedings of the 2012 Federa- ted Conference on Computer Science and Information Systems. Pis- cataway, NJ: IEEE Press, 2012:1397-1401.
  • 2LORINA N, [RINA M, ADINA M F. Foruaal specification and veri- fication of concurrent Agents in Event-B [ C]// Proceedings of the 19th International Conference on Control Systems and Computer Sci- ence. Piscataway, NJ: IEEE Press, 2013:155-161.
  • 3MOHAMED T, MOHAMED M, DOMINIQUE M. From event-B specifications to programs for distributed algorithms [ C]/! Work- shops on Enabling Technologies: Infrastructure for Collaborative En- terprises. Piscatawa,/, NJ: IEEE Press, 2013:104-109.
  • 4PEREVERZEVA I, TROUB|TSYNA E, LAIBINIS L. Formal devel- opment of critical multi-Agent systems: a refinement approach [ C]// Proceedings of the 9th European Dependable Computing Con- ference. Piscataway, NJ: IEEE Press, 2012: 156- 161.
  • 5TRUONG N-T, TRINH T-B, NGUYEN V-H. Coordinated consen- sus ana|ysis of multi-Agent systems using event-B [ C]// SEFM'09: Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods. Piscataway, NJ: IEEE Press, 2009:201-209.
  • 6Abrial J R.Modeling in Event-B:System and software engineering[M].Cambridge:Cambridge University Press,2010.
  • 7Abrial 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.
  • 8Damchoom 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.
  • 9Shi 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.
  • 10Shi 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.

引证文献2

二级引证文献2

计算机应用
2012年 第12期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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