亲爱的研友该休息了!由于当前在线用户较少,发布求助请尽量完整地填写文献信息,科研通机器人24小时在线,伴您度过漫漫科研夜!身体可是革命的本钱,早点休息,好梦!

Concurrent Algorithms in SPIN Model Checker

正确性 Promela公司 活泼 模型检查 计算机科学 互斥 算法 断言 程序设计语言 线性时序逻辑 时态逻辑 理论计算机科学
作者
M. Saqib Nawaz,Hussam Ali,M. Ikram Ullah Lali
标识
DOI:10.1109/fit.2016.043
摘要

Analysis and finding errors in concurrent software/system particularly when it is used in safety or industrial critical systems is gaining more and more attention. Software testing is an important technique for finding errors, however for concurrent algorithms, testing often does not ensure correctness or absence of errors. The model checker SPIN is widely and successfully used to formally verify the correctness requirements for systems of concurrently executing processes. Software/system model is first developed in PROMELA modeling language and SPIN model checker accepts correctness claims that are declared as linear temporal logic (LTL) formulas. In this article, two famous concurrent algorithms for mutual exclusion problem (Bakery algorithm and Dekker algorithm) are analyzed and formally verified in SPIN. Mutual exclusion for both algorithms is verified with in-line assertion and as correctness claims with the help of LTL formulas. Furthermore, safety and liveness properties of both algorithms are verified with LTL formulas.
最长约 10秒,即可获得该文献文件

科研通智能强力驱动
Strongly Powered by AbleSci AI
更新
PDF的下载单位、IP信息已删除 (2025-6-4)

科研通是完全免费的文献互助平台,具备全网最快的应助速度,最高的求助完成率。 对每一个文献求助,科研通都将尽心尽力,给求助人一个满意的交代。
实时播报
Huay完成签到 ,获得积分10
1秒前
tingting9发布了新的文献求助10
1秒前
英俊的铭应助科研通管家采纳,获得10
5秒前
5秒前
kd1412应助科研通管家采纳,获得10
5秒前
善学以致用应助吴昕昕采纳,获得10
7秒前
tingting9完成签到,获得积分10
9秒前
吾日三省吾身完成签到,获得积分10
14秒前
sola完成签到 ,获得积分10
29秒前
DreamMaker完成签到 ,获得积分10
31秒前
VVV完成签到,获得积分10
33秒前
46秒前
48秒前
_ban发布了新的文献求助10
51秒前
小黄鸭完成签到,获得积分10
55秒前
滴滴哒发布了新的文献求助10
1分钟前
李李原上草完成签到 ,获得积分10
1分钟前
超级的千青完成签到 ,获得积分10
1分钟前
1分钟前
Bio应助又来注水了采纳,获得30
1分钟前
万能图书馆应助爹爹采纳,获得10
1分钟前
layman完成签到,获得积分10
1分钟前
郭郭完成签到 ,获得积分10
1分钟前
FL完成签到 ,获得积分10
1分钟前
科研通AI5应助sljzhangbiao11采纳,获得10
1分钟前
又来注水了完成签到,获得积分10
1分钟前
快乐海豚完成签到 ,获得积分10
2分钟前
科研通AI5应助科研通管家采纳,获得10
2分钟前
科研狗的春天完成签到 ,获得积分10
2分钟前
Lucas应助董可以采纳,获得10
2分钟前
2分钟前
Aqib发布了新的文献求助10
2分钟前
2分钟前
科研通AI5应助西瓜嘻嘻嘻采纳,获得10
2分钟前
吴昕昕发布了新的文献求助10
2分钟前
未晚完成签到 ,获得积分10
2分钟前
香蕉觅云应助Aqib采纳,获得10
2分钟前
早晨发布了新的文献求助10
2分钟前
孤鸿.完成签到 ,获得积分10
2分钟前
2分钟前
高分求助中
The Mother of All Tableaux: Order, Equivalence, and Geometry in the Large-scale Structure of Optimality Theory 3000
A new approach to the extrapolation of accelerated life test data 1000
ACSM’s Guidelines for Exercise Testing and Prescription, 12th edition 500
Indomethacinのヒトにおける経皮吸収 400
Phylogenetic study of the order Polydesmida (Myriapoda: Diplopoda) 370
基于可调谐半导体激光吸收光谱技术泄漏气体检测系统的研究 350
Robot-supported joining of reinforcement textiles with one-sided sewing heads 320
热门求助领域 (近24小时)
化学 材料科学 医学 生物 工程类 有机化学 生物化学 物理 内科学 纳米技术 计算机科学 化学工程 复合材料 遗传学 基因 物理化学 催化作用 冶金 细胞生物学 免疫学
热门帖子
关注 科研通微信公众号,转发送积分 3990020
求助须知:如何正确求助?哪些是违规求助? 3532077
关于积分的说明 11256276
捐赠科研通 3270943
什么是DOI,文献DOI怎么找? 1805139
邀请新用户注册赠送积分活动 882270
科研通“疑难数据库(出版商)”最低求助积分说明 809228