SPIN Model Checking for the BEE System

被引：0
作者：
Yamada, Chikatoshi [1 ]
Ganti, Sudhakar [2 ]
Miller, D. Michael [2 ]
机构：
[1] Okinawa Natl Coll Technol, Dept Informat & Commun Syst Engn, Nago, Okinawa, Japan
[2] Univ Victoria, Dept Comp Sci, Victoria, BC V8W 2Y2, Canada
来源：
TENCON 2015 - 2015 IEEE REGION 10 CONFERENCE | 2015年
关键词：
D O I：
暂无
中图分类号：
TM [电工技术]; TN [电子技术、通信技术];
学科分类号：
0808 ; 0809 ;
摘要：
This paper discusses the application of SPIN model checking to BEE platform Simulink models. In particular, Simulink Stateflow models are added to BEE platform models to facilitate checking using the SPIN tool. Algorithms are given for doing the necessary translations and we present empirical results to illustrate the application of the approach introduced in this paper. We also show how our tools allow SPIN to be used for model checking nondeterministic behaviour of BEE models.
引用
收藏
页数：6
相关论文
共 15 条
  • [1] Agrawal A., 2004, Electronic Notes in Theoretical Computer Science, V109, P43
  • [2] [Anonymous], 2004, P 13 INT C WORLD WID, DOI DOI 10.1145/988672.988756
  • [3] Clarke J.E. M., 1999, Model Checking
  • [4] Dahmoune O., 2010, Proceedings of the 2010 11th International Workshop on Microprocessor Test and Verification (MTV), P47, DOI 10.1109/MTV.2010.17
  • [5] Fu X, 2004, LECT NOTES COMPUT SC, V3114, P510
  • [6] Holzmann G., 2003, The SPIN Model Checker: Primer and Reference Manual, V1st
  • [7] Joshi A, 2005, LECT NOTES COMPUT SC, V3688, P122
  • [8] Leitner F., 2008, THESIS
  • [9] Rothman J, 2012, 2012 INTERNATIONAL CONFERENCE ON EMBEDDED COMPUTER SYSTEMS (SAMOS): ARCHITECTURES, MODELING AND SIMULATION, P277, DOI 10.1109/SAMOS.2012.6404186
  • [10] Scaife N., 2004, Proceedings of the 4th ACM international conference on Embedded software, P259
12