Probabilistic modelling and verification using RoboChart and PRISM

RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The ex...

Full description

Saved in:
Bibliographic Details
Published in:Software and systems modeling 2022-04, Vol.21 (2), p.667-716
Main Authors: Ye, Kangfeng, Cavalcanti, Ana, Foster, Simon, Miyazawa, Alvaro, Woodcock, Jim
Format: Article
Language:English
Subjects:
Automation
Compilers
Computer Science
Control algorithms
Domain specific languages
Information Systems Applications (incl.Internet)
Interpreters
IT in Business
Language
Modelling
Probabilistic models
Programming Languages
Programming Techniques
Regular Paper
Robotics
Robots
Semantics
Software Engineering
Software Engineering/Programming and Operating Systems
State machines
Statistical analysis
Temporal logic
Uncertainty
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c363t-179aa43e3768c8d04ef1c42eb89155ed02e6d1e552c06fd03a671b71087d2c363
cites cdi_FETCH-LOGICAL-c363t-179aa43e3768c8d04ef1c42eb89155ed02e6d1e552c06fd03a671b71087d2c363
container_end_page 716
container_issue 2
container_start_page 667
container_title Software and systems modeling
container_volume 21
creator Ye, Kangfeng
Cavalcanti, Ana
Foster, Simon
Miyazawa, Alvaro
Woodcock, Jim
description RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.
doi_str_mv 10.1007/s10270-021-00916-8
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_journals_2647959221</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>2647959221</sourcerecordid><originalsourceid>FETCH-LOGICAL-c363t-179aa43e3768c8d04ef1c42eb89155ed02e6d1e552c06fd03a671b71087d2c363</originalsourceid><addsrcrecordid>eNp9kF1LwzAUhoMoOOb-gFcFr6vnJGnSXOrwYzBxTL0OaZvOSNfMpBX893ar6J1X53B43vfAQ8g5wiUCyKuIQCWkQDEFUCjS_IhMUKBKkUl-_LsLcUpmMboCgFOluBATcrMKvjCFa1zsXJlsfWWbxrWbxLRV8mmDq11pOufbpI_789oXfv5mQncAVuvF8-MZOalNE-3sZ07J693ty_whXT7dL-bXy7RkgnUpSmUMZ5ZJkZd5BdzWWHJqi1xhltkKqBUV2iyjJYi6AmaExEIi5LKi-4opuRh7d8F_9DZ2-t33oR1eaiq4VJmiFAeKjlQZfIzB1noX3NaEL42g97r0qEsPuvRBl86HEBtDcYDbjQ1_1f-kvgF4ZmvB</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>2647959221</pqid></control><display><type>article</type><title>Probabilistic modelling and verification using RoboChart and PRISM</title><source>Springer Nature</source><creator>Ye, Kangfeng ; Cavalcanti, Ana ; Foster, Simon ; Miyazawa, Alvaro ; Woodcock, Jim</creator><creatorcontrib>Ye, Kangfeng ; Cavalcanti, Ana ; Foster, Simon ; Miyazawa, Alvaro ; Woodcock, Jim</creatorcontrib><description>RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.</description><identifier>ISSN: 1619-1366</identifier><identifier>EISSN: 1619-1374</identifier><identifier>DOI: 10.1007/s10270-021-00916-8</identifier><language>eng</language><publisher>Berlin/Heidelberg: Springer Berlin Heidelberg</publisher><subject>Automation ; Compilers ; Computer Science ; Control algorithms ; Domain specific languages ; Information Systems Applications (incl.Internet) ; Interpreters ; IT in Business ; Language ; Modelling ; Probabilistic models ; Programming Languages ; Programming Techniques ; Regular Paper ; Robotics ; Robots ; Semantics ; Software Engineering ; Software Engineering/Programming and Operating Systems ; State machines ; Statistical analysis ; Temporal logic ; Uncertainty ; Verification</subject><ispartof>Software and systems modeling, 2022-04, Vol.21 (2), p.667-716</ispartof><rights>The Author(s) 2021</rights><rights>The Author(s) 2021. This work is published under http://creativecommons.org/licenses/by/4.0/ (the “License”). Notwithstanding the ProQuest Terms and Conditions, you may use this content in accordance with the terms of the License.</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c363t-179aa43e3768c8d04ef1c42eb89155ed02e6d1e552c06fd03a671b71087d2c363</citedby><cites>FETCH-LOGICAL-c363t-179aa43e3768c8d04ef1c42eb89155ed02e6d1e552c06fd03a671b71087d2c363</cites><orcidid>0000-0003-2460-7926</orcidid></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,776,780,27901,27902</link.rule.ids></links><search><creatorcontrib>Ye, Kangfeng</creatorcontrib><creatorcontrib>Cavalcanti, Ana</creatorcontrib><creatorcontrib>Foster, Simon</creatorcontrib><creatorcontrib>Miyazawa, Alvaro</creatorcontrib><creatorcontrib>Woodcock, Jim</creatorcontrib><title>Probabilistic modelling and verification using RoboChart and PRISM</title><title>Software and systems modeling</title><addtitle>Softw Syst Model</addtitle><description>RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.</description><subject>Automation</subject><subject>Compilers</subject><subject>Computer Science</subject><subject>Control algorithms</subject><subject>Domain specific languages</subject><subject>Information Systems Applications (incl.Internet)</subject><subject>Interpreters</subject><subject>IT in Business</subject><subject>Language</subject><subject>Modelling</subject><subject>Probabilistic models</subject><subject>Programming Languages</subject><subject>Programming Techniques</subject><subject>Regular Paper</subject><subject>Robotics</subject><subject>Robots</subject><subject>Semantics</subject><subject>Software Engineering</subject><subject>Software Engineering/Programming and Operating Systems</subject><subject>State machines</subject><subject>Statistical analysis</subject><subject>Temporal logic</subject><subject>Uncertainty</subject><subject>Verification</subject><issn>1619-1366</issn><issn>1619-1374</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2022</creationdate><recordtype>article</recordtype><recordid>eNp9kF1LwzAUhoMoOOb-gFcFr6vnJGnSXOrwYzBxTL0OaZvOSNfMpBX893ar6J1X53B43vfAQ8g5wiUCyKuIQCWkQDEFUCjS_IhMUKBKkUl-_LsLcUpmMboCgFOluBATcrMKvjCFa1zsXJlsfWWbxrWbxLRV8mmDq11pOufbpI_789oXfv5mQncAVuvF8-MZOalNE-3sZ07J693ty_whXT7dL-bXy7RkgnUpSmUMZ5ZJkZd5BdzWWHJqi1xhltkKqBUV2iyjJYi6AmaExEIi5LKi-4opuRh7d8F_9DZ2-t33oR1eaiq4VJmiFAeKjlQZfIzB1noX3NaEL42g97r0qEsPuvRBl86HEBtDcYDbjQ1_1f-kvgF4ZmvB</recordid><startdate>20220401</startdate><enddate>20220401</enddate><creator>Ye, Kangfeng</creator><creator>Cavalcanti, Ana</creator><creator>Foster, Simon</creator><creator>Miyazawa, Alvaro</creator><creator>Woodcock, Jim</creator><general>Springer Berlin Heidelberg</general><general>Springer Nature B.V</general><scope>C6C</scope><scope>AAYXX</scope><scope>CITATION</scope><scope>3V.</scope><scope>7SC</scope><scope>7XB</scope><scope>8AL</scope><scope>8AO</scope><scope>8FD</scope><scope>8FE</scope><scope>8FG</scope><scope>8FK</scope><scope>ABUWG</scope><scope>AFKRA</scope><scope>ARAPS</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>GNUQQ</scope><scope>HCIFZ</scope><scope>JQ2</scope><scope>K7-</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope><scope>M0N</scope><scope>P5Z</scope><scope>P62</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope><scope>PRINS</scope><scope>Q9U</scope><orcidid>https://orcid.org/0000-0003-2460-7926</orcidid></search><sort><creationdate>20220401</creationdate><title>Probabilistic modelling and verification using RoboChart and PRISM</title><author>Ye, Kangfeng ; Cavalcanti, Ana ; Foster, Simon ; Miyazawa, Alvaro ; Woodcock, Jim</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c363t-179aa43e3768c8d04ef1c42eb89155ed02e6d1e552c06fd03a671b71087d2c363</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2022</creationdate><topic>Automation</topic><topic>Compilers</topic><topic>Computer Science</topic><topic>Control algorithms</topic><topic>Domain specific languages</topic><topic>Information Systems Applications (incl.Internet)</topic><topic>Interpreters</topic><topic>IT in Business</topic><topic>Language</topic><topic>Modelling</topic><topic>Probabilistic models</topic><topic>Programming Languages</topic><topic>Programming Techniques</topic><topic>Regular Paper</topic><topic>Robotics</topic><topic>Robots</topic><topic>Semantics</topic><topic>Software Engineering</topic><topic>Software Engineering/Programming and Operating Systems</topic><topic>State machines</topic><topic>Statistical analysis</topic><topic>Temporal logic</topic><topic>Uncertainty</topic><topic>Verification</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Ye, Kangfeng</creatorcontrib><creatorcontrib>Cavalcanti, Ana</creatorcontrib><creatorcontrib>Foster, Simon</creatorcontrib><creatorcontrib>Miyazawa, Alvaro</creatorcontrib><creatorcontrib>Woodcock, Jim</creatorcontrib><collection>SpringerOpen</collection><collection>CrossRef</collection><collection>ProQuest Central (Corporate)</collection><collection>Computer and Information Systems Abstracts</collection><collection>ProQuest Central (purchase pre-March 2016)</collection><collection>Computing Database (Alumni Edition)</collection><collection>ProQuest Pharma Collection</collection><collection>Technology Research Database</collection><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>ProQuest Central (Alumni) (purchase pre-March 2016)</collection><collection>ProQuest Central (Alumni)</collection><collection>ProQuest Central</collection><collection>Advanced Technologies &amp; Aerospace Database‎ (1962 - current)</collection><collection>ProQuest Central Essentials</collection><collection>AUTh Library subscriptions: ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central</collection><collection>ProQuest Central Student</collection><collection>SciTech Premium Collection (Proquest) (PQ_SDU_P3)</collection><collection>ProQuest Computer Science Collection</collection><collection>Computer Science Database</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><collection>Computing Database</collection><collection>ProQuest advanced technologies &amp; aerospace journals</collection><collection>ProQuest Advanced Technologies &amp; Aerospace Collection</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><collection>ProQuest Central China</collection><collection>ProQuest Central Basic</collection><jtitle>Software and systems modeling</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Ye, Kangfeng</au><au>Cavalcanti, Ana</au><au>Foster, Simon</au><au>Miyazawa, Alvaro</au><au>Woodcock, Jim</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Probabilistic modelling and verification using RoboChart and PRISM</atitle><jtitle>Software and systems modeling</jtitle><stitle>Softw Syst Model</stitle><date>2022-04-01</date><risdate>2022</risdate><volume>21</volume><issue>2</issue><spage>667</spage><epage>716</epage><pages>667-716</pages><issn>1619-1366</issn><eissn>1619-1374</eissn><abstract>RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.</abstract><cop>Berlin/Heidelberg</cop><pub>Springer Berlin Heidelberg</pub><doi>10.1007/s10270-021-00916-8</doi><tpages>50</tpages><orcidid>https://orcid.org/0000-0003-2460-7926</orcidid><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 1619-1366
ispartof Software and systems modeling, 2022-04, Vol.21 (2), p.667-716
issn 1619-1366
1619-1374
language eng
recordid cdi_proquest_journals_2647959221
source Springer Nature
subjects Automation
Compilers
Computer Science
Control algorithms
Domain specific languages
Information Systems Applications (incl.Internet)
Interpreters
IT in Business
Language
Modelling
Probabilistic models
Programming Languages
Programming Techniques
Regular Paper
Robotics
Robots
Semantics
Software Engineering
Software Engineering/Programming and Operating Systems
State machines
Statistical analysis
Temporal logic
Uncertainty
Verification
title Probabilistic modelling and verification using RoboChart and PRISM
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-02-13T14%3A21%3A11IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Probabilistic%20modelling%20and%20verification%20using%20RoboChart%20and%20PRISM&rft.jtitle=Software%20and%20systems%20modeling&rft.au=Ye,%20Kangfeng&rft.date=2022-04-01&rft.volume=21&rft.issue=2&rft.spage=667&rft.epage=716&rft.pages=667-716&rft.issn=1619-1366&rft.eissn=1619-1374&rft_id=info:doi/10.1007/s10270-021-00916-8&rft_dat=%3Cproquest_cross%3E2647959221%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c363t-179aa43e3768c8d04ef1c42eb89155ed02e6d1e552c06fd03a671b71087d2c363%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=2647959221&rft_id=info:pmid/&rfr_iscdi=true