Repositorio UVigo

Formal verification for task description languages. A Petri Net approach

Investigo Repository

Formal verification for task description languages. A Petri Net approach

López Fernández, Joaquín; Santana Alonso, Alejandro Alejo; Diaz Cacho Medina, Miguel Ramon
 
DATE : 2019-11-14
UNIVERSAL IDENTIFIER : http://hdl.handle.net/11093/1569
UNESCO SUBJECT : 1203.04 Inteligencia Artificial ; 33 Ciencias Tecnológicas
DOCUMENT TYPE : article

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 ... [+]
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. [-]

Show full item record



Files in this item

Creative Commons Attribution
(CC BY) license Except where otherwise noted, this item's license is described as Creative Commons Attribution (CC BY) license
2013 Universidade de Vigo, Todos los derechos reservados
Calidad So9001