Blog
About

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

      Formal Verification for Task Description Languages. A Petri Net Approach

      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

          One of the main challenges in verifying robotic systems is its asynchronous interaction with an unstructured environment, observed by imperfect sensors. Autonomous robot systems usually require some language to support task-level control. This paper presents an effective approach to apply formal verification methods for that kind of language. A main contribution of this method is to avoid modeling the robotic system with a specific formalism. The approach translates the task-level control models into a Petri net (PN) based representation. This is used to define new methods to analyze some task properties such as liveness, deadlock-freeness and terminability. The approach has been applied to the Task Description Language (TDL) and it is illustrated by experiments. The final goal is to create new tools within the application development environment to include formal verification as part of the normal software development cycle. The TDL to PN translator uses the Petri Net Markup Language (PNML) as its file format. This format permits interoperability with other Petri net tools that can also be used to analyze the PNs.

          Related collections

          Most cited references 38

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

          Petri nets: Properties, analysis and applications

           T Murata (1989)
            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Symbolic model checking: 1020 States and beyond

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

              Parallel program schemata

                Bookmark

                Author and article information

                Journal
                Sensors (Basel)
                Sensors (Basel)
                sensors
                Sensors (Basel, Switzerland)
                MDPI
                1424-8220
                14 November 2019
                November 2019
                : 19
                : 22
                Affiliations
                Dep. Ingeniería de Sistemas y Automática, University of Vigo, 36200 Vigo, Spain; asantana@ 123456uvigo.es (A.S.-A.); mcacho@ 123456uvigo.es (M.D.-C.M.)
                Author notes
                [* ]Correspondence: joaquin@ 123456uvigo.es ; Tel.: +34-986-812-231
                Article
                sensors-19-04965
                10.3390/s19224965
                6891290
                31739526
                © 2019 by the authors.

                Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license ( http://creativecommons.org/licenses/by/4.0/).

                Categories
                Article

                Comments

                Comment on this article