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

System verification via Model‐Checking: A case study of an autonomous multi‐differential drive robot

系统建模语言 模型检查 计算机科学 形式验证 形式化方法 过程(计算) 程序设计语言 活动图 建模语言 帧(网络) 正式规范 软件工程 统一建模语言 系统工程 工程类 软件 电信
作者
Ibukun Phillips,C. Robert Kenley
出处
期刊:INCOSE International Symposium [Wiley]
卷期号:33 (1): 17-31
标识
DOI:10.1002/iis2.13006
摘要

Abstract Model‐Based Systems Engineering (MBSE) has been utilized in practice to design and behavioral modeling cyber‐physical systems. The Vee model helps frame MBSE's lifecycle approach, with system verification a vital aspect of the qualification process. However, popular modeling language tools in MBSE, such as Systems Modeling Language (SysML), are incapable of formally verifying these systems. Model checking allows for the development of formal system models similar in abstraction to SysML models for automatically checking if these formal models satisfy formal specifications. We propose an approach to translate behavioral diagrams in SysML, such as state‐machine diagrams, to the popular symbolic model checker NuSMV for formal verification. As a case study, we apply this process to autonomous multi‐differential drive robots (DDR). Subsequently, the NuSMV model is verified against some formal operational specifications obtained from the requirements diagram of the DDR. This system verification approach can help System Engineers identify design flaws or incorrect modeling or specifications that could be missed during the design phase through the results of the model checking process.
最长约 10秒,即可获得该文献文件

科研通智能强力驱动
Strongly Powered by AbleSci AI
更新
大幅提高文件上传限制,最高150M (2024-4-1)

科研通是完全免费的文献互助平台,具备全网最快的应助速度,最高的求助完成率。 对每一个文献求助,科研通都将尽心尽力,给求助人一个满意的交代。
实时播报
梨炒栗子完成签到 ,获得积分10
9秒前
SolderOH完成签到,获得积分10
9秒前
额123没名完成签到 ,获得积分10
11秒前
大个应助yao采纳,获得10
22秒前
24秒前
柳Iris发布了新的文献求助10
27秒前
CodeCraft应助rui采纳,获得10
29秒前
30秒前
杳鸢应助科研通管家采纳,获得10
31秒前
Hahaha发布了新的文献求助10
31秒前
myg123完成签到 ,获得积分10
33秒前
吴彦祖发布了新的文献求助10
35秒前
子爵木完成签到 ,获得积分10
37秒前
柳Iris完成签到,获得积分20
41秒前
在水一方应助兴奋元冬采纳,获得10
46秒前
47秒前
羲和完成签到 ,获得积分10
50秒前
Hahaha完成签到,获得积分10
54秒前
Qvby3完成签到 ,获得积分10
58秒前
可爱以冬完成签到 ,获得积分10
1分钟前
英姑应助oscar采纳,获得10
1分钟前
科目三应助whoknowsname采纳,获得10
1分钟前
泠风来完成签到,获得积分10
1分钟前
123321完成签到 ,获得积分10
1分钟前
烟花应助inRe采纳,获得30
1分钟前
bkagyin应助miuwu采纳,获得10
1分钟前
Betty完成签到 ,获得积分10
1分钟前
1分钟前
Carrots完成签到 ,获得积分10
1分钟前
1分钟前
七七关注了科研通微信公众号
1分钟前
简单的思菱完成签到 ,获得积分10
1分钟前
Ade阿德完成签到 ,获得积分10
1分钟前
http完成签到,获得积分20
1分钟前
惠民发布了新的文献求助20
1分钟前
1分钟前
研友_VZG7GZ应助http采纳,获得10
1分钟前
完美世界应助catherlink采纳,获得10
1分钟前
2分钟前
2分钟前
高分求助中
The late Devonian Standard Conodont Zonation 2000
Nickel superalloy market size, share, growth, trends, and forecast 2023-2030 2000
The Lali Section: An Excellent Reference Section for Upper - Devonian in South China 1500
Very-high-order BVD Schemes Using β-variable THINC Method 890
Mantiden: Faszinierende Lauerjäger Faszinierende Lauerjäger 800
PraxisRatgeber: Mantiden: Faszinierende Lauerjäger 800
A new species of Coccus (Homoptera: Coccoidea) from Malawi 500
热门求助领域 (近24小时)
化学 医学 生物 材料科学 工程类 有机化学 生物化学 物理 内科学 纳米技术 计算机科学 化学工程 复合材料 基因 遗传学 催化作用 物理化学 免疫学 量子力学 细胞生物学
热门帖子
关注 科研通微信公众号,转发送积分 3256828
求助须知:如何正确求助?哪些是违规求助? 2898945
关于积分的说明 8303123
捐赠科研通 2568188
什么是DOI,文献DOI怎么找? 1394905
科研通“疑难数据库(出版商)”最低求助积分说明 652924
邀请新用户注册赠送积分活动 630631