Show simple item record

dc.contributor.authorLópez Fernández, Joaquín 
dc.contributor.authorSantana Alonso, Alejandro Alejo 
dc.contributor.authorDiaz Cacho Medina, Miguel Ramon 
dc.date.accessioned2020-10-06T06:54:52Z
dc.date.available2020-10-06T06:54:52Z
dc.date.issued2019-11-14
dc.identifier.citationSensors, 19(22): 4965 (2019)spa
dc.identifier.issn14248220
dc.identifier.urihttp://hdl.handle.net/11093/1569
dc.description.abstractOne 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.spa
dc.description.sponsorshipMinisterio de Economía y Competitividad | Ref. (TRA2015-70501-C2-2-R)spa
dc.language.isoengspa
dc.publisherSensorsspa
dc.rightsCreative Commons Attribution (CC BY) license
dc.rights.uri(http://creativecommons.org/licenses/by/4.0/)
dc.titleFormal verification for task description languages. A Petri Net approachspa
dc.typearticlespa
dc.rights.accessRightsopenAccessspa
dc.identifier.doi10.3390/s19224965
dc.identifier.editorhttps://www.mdpi.com/1424-8220/19/22/4965spa
dc.publisher.departamentoEnxeñaría de sistemas e automáticaspa
dc.publisher.grupoinvestigacionRobótica e Sistemas Intelixentesspa
dc.publisher.grupoinvestigacionGrupo de Control non Liñalspa
dc.subject.unesco1203.04 Inteligencia Artificialspa
dc.subject.unesco33 Ciencias Tecnológicasspa
dc.date.updated2020-10-02T11:28:45Z
dc.computerCitationpub_title=Sensors|volume=19|journal_number=22|start_pag=4965|end_pag=spa


Files in this item

[PDF]

    Show simple item record

    Creative Commons Attribution
(CC BY) license
    Except where otherwise noted, this item's license is described as Creative Commons Attribution (CC BY) license