20
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Probabilistic modelling and verification using RoboChart and PRISM

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Most cited references45

          • Record: found
          • Abstract: not found
          • Article: not found

          A logic for reasoning about time and reliability

            Bookmark
            • Record: found
            • Abstract: not found
            • Book: not found

            Isabelle/HOL

              Bookmark
              • Record: found
              • Abstract: not found
              • Book: not found

              Markov Decision Processes

                Bookmark

                Author and article information

                Contributors
                Journal
                Software and Systems Modeling
                Softw Syst Model
                Springer Science and Business Media LLC
                1619-1366
                1619-1374
                April 2022
                October 03 2021
                April 2022
                : 21
                : 2
                : 667-716
                Article
                10.1007/s10270-021-00916-8
                4d883d02-3b58-482e-8073-2f032cf30208
                © 2022

                https://creativecommons.org/licenses/by/4.0

                https://creativecommons.org/licenses/by/4.0

                History

                Comments

                Comment on this article

                scite_
                0
                0
                0
                0
                Smart Citations
                0
                0
                0
                0
                Citing PublicationsSupportingMentioningContrasting
                View Citations

                See how this article has been cited at scite.ai

                scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.

                Similar content487

                Cited by1

                Most referenced authors267