基于SPIN求解狼和白菜过河问题
Based on SPIN to Solve the Problem of Wolf and Cabbage Across the River
摘要
模型验证是数理逻辑在现实中的一个重要应用。文章基于Promela语言,用spin工具检验数理逻辑的一个经典案例——狼和白菜过河问题。
Model validation is a very important part of the mathematical logic in reality.This paper,based on the language of Premela,uses the tool of spin to inspect a classic example of the mathematical logic——the problem of wolf and cabbage across the river.
出处
《铜仁职业技术学院学报》
2014年第2期35-37,共3页
Academic forum of Tongren Polytechnic College
二级参考文献17
-
1骆翔宇,苏开乐,杨晋吉.有界模型检测同步多智体系统的时态认知逻辑[J].软件学报,2006,17(12):2485-2498. 被引量：13
-
2Fu Xiang, Bultan T, Su Jianwei. Analysis of Interacting BPEL Web Services[C]//Proc. of the 13th Int'l Conf. on World Wide Web. [S. 1.]: ACM Press, 2004.
-
3Lomuscio A. Verifying Temporal Epistemic Properties of Web Service Compositions[C]//Proc. of the 5th Int'l Conf. on Service Oriented Computing. Vienna, Austria: [s. n.], 2007.
-
4Fagin R. Reasoning About Knowledge[M]. Cambridge, MA, USA: MIT Press, 1995.
-
5Luo Xiangyu, Su Kaile, Abdul S, et al. Verification of Multi-agent Systems via Bounded Model Checking[C]//Proc. of the 19th Australian Joint Conference on Artificial Intelligence. Hobart, Australia: [s. n.], 2006.
-
6Su Kaile, Abdul S, Luo Xiangyu. Model Checking Temporal Logics of Knowledge via OBDDs[J]. The Computer Journal, 2007, 50(4): 403-420.
-
7HuthM,RyanM.面向计算机科学的数理逻辑系统建模与推理[M].北京:机械工业出版社,2007.
-
8Poll E. Modeling and analysis using Uppaal[ OL]. [ 2011 -07 -01]. http ://www. cs. ru. nl/E. Poll/Teaching/Uppaal/.
-
9Basagiannis S, Katsaros P, Pombortsis A. An intruder model with mes- sage inspection for model checking security protocols[J]. Computers and Security,2010,29 : 16 - 34.
-
10Islam S M S, Sqalli M H, Khan S. Modeling and Formal Verification of DHCP Using SPIN[ J ]. International Journal of Computer Science and Applications,2006,6 ( 3 ) : 145 - 159.
-
1赵蔚.Windows 上的Unix环境：CygWin[J].开放系统世界,2002(8):46-47.
-
2马超,林红昌,丁佐华.基于UML和Petri网的建模及其验证[J].浙江理工大学学报（自然科学版）,2010,27(6):889-894. 被引量：1
-
3刁红艳.谈“过河”问题在“死锁”中的运用[J].无锡南洋职业技术学院论丛,2007,0(2):33-34. 被引量：2
-
4白秀玲,张蕾,邱涌,宋晓莉,张孝国,张明川.过河问题的算法改进[J].福建电脑,2009,25(7):13-14.
-
5石颖.利用SPIN实现对OpenFlow协议的形式化验证[J].计算机安全,2014(3):38-43. 被引量：2
-
6胡文生,李祥.Win32平台下的UNIX原始套接字编程及应用[J].电脑与信息技术,2005,13(2):44-46.
-
7肖杨,李国旗.基于Alloy求解过河问题[J].计算机应用与软件,2010,27(10):165-167. 被引量：1
-
8王彩云.基于windows 2003构建DNS服务器的两种方法[J].电脑知识与技术（过刊）,2012,18(1X):288-290. 被引量：2
-
9赵天翔,李冬梅.在Windows操作系统中构建Linux环境[J].福建电脑,2008,24(10):172-172. 被引量：2
-
10邹秀斌.八人过河问题的Java编程实现[J].电脑编程技巧与维护,2016(21):14-19.
