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)

科研通是完全免费的文献互助平台,具备全网最快的应助速度,最高的求助完成率。 对每一个文献求助,科研通都将尽心尽力,给求助人一个满意的交代。
实时播报
西早07完成签到,获得积分10
刚刚
Meng完成签到,获得积分10
1秒前
Neo完成签到,获得积分10
2秒前
keyaner完成签到,获得积分10
4秒前
童林艳完成签到,获得积分10
4秒前
ECHO完成签到,获得积分10
6秒前
Lucas应助Fang Xianxin采纳,获得10
7秒前
xiaoyao完成签到,获得积分10
8秒前
asss完成签到,获得积分10
8秒前
Y123发布了新的文献求助30
9秒前
LOVER完成签到 ,获得积分10
10秒前
松松完成签到 ,获得积分10
10秒前
12秒前
nater4ver完成签到,获得积分10
13秒前
UU发布了新的文献求助10
15秒前
超帅鸭子完成签到,获得积分10
15秒前
LXZ完成签到,获得积分10
15秒前
依惜完成签到,获得积分10
15秒前
zhaokunfeng关注了科研通微信公众号
15秒前
赫青亦完成签到 ,获得积分10
15秒前
exy完成签到,获得积分10
16秒前
zhaohu47完成签到,获得积分10
17秒前
超帅鸭子发布了新的文献求助10
17秒前
每每反完成签到,获得积分10
19秒前
凡凡完成签到 ,获得积分10
20秒前
21秒前
呆鹅喵喵完成签到,获得积分10
21秒前
忧心的洙完成签到,获得积分10
22秒前
123完成签到,获得积分10
22秒前
青青草完成签到,获得积分10
24秒前
Fang Xianxin完成签到,获得积分20
24秒前
yue发布了新的文献求助10
24秒前
小甘看世界完成签到,获得积分0
26秒前
量子星尘发布了新的文献求助10
26秒前
张今天也要做科研呀完成签到,获得积分10
27秒前
nater3ver完成签到,获得积分10
28秒前
28秒前
自然怀梦完成签到,获得积分10
28秒前
轻歌水越完成签到 ,获得积分10
28秒前
执意完成签到 ,获得积分10
29秒前
高分求助中
【提示信息,请勿应助】关于scihub 10000
Les Mantodea de Guyane: Insecta, Polyneoptera [The Mantids of French Guiana] 3000
徐淮辽南地区新元古代叠层石及生物地层 3000
The Mother of All Tableaux: Order, Equivalence, and Geometry in the Large-scale Structure of Optimality Theory 3000
Handbook of Industrial Diamonds.Vol2 1100
Global Eyelash Assessment scale (GEA) 1000
Picture Books with Same-sex Parented Families: Unintentional Censorship 550
热门求助领域 (近24小时)
化学 材料科学 医学 生物 工程类 有机化学 生物化学 物理 内科学 纳米技术 计算机科学 化学工程 复合材料 遗传学 基因 物理化学 催化作用 冶金 细胞生物学 免疫学
热门帖子
关注 科研通微信公众号,转发送积分 4038303
求助须知:如何正确求助?哪些是违规求助? 3576013
关于积分的说明 11374210
捐赠科研通 3305780
什么是DOI,文献DOI怎么找? 1819322
邀请新用户注册赠送积分活动 892672
科研通“疑难数据库(出版商)”最低求助积分说明 815029