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.

Many distributed frameworks use a message-oriented middleware to interchange information among several independent distributed modules. Those modules make up complex systems implementing basic actions and reporting events about their state. This paper introduces the Message Interpreted Petri Net (MIPN) model to design, analyze, and execute the central control of these middleware systems. The MIPN is a new Petri net extension that adds message-based high-level information communications and hierarchic capabilities. It also contributes to the definition and study of new properties such as terminability for the hierarchy-wide analysis of a system. Special attention is given to the analyzability of the model. Useful relations between the individual properties of each MIPN and the global properties of a hierarchic MIPNs system are extracted through a mathematical analysis of the model. The goal is to analyze each net separately and then build up the properties of the whole system. This results in a great aid for the programmer and optimizes the development process. This paper also shows the actual integration of this new MIPN model in different robot control frameworks to design, analyze, execute, monitor, log, and debug tasks in such heterogeneous systems. Finally, some applications created with this framework in the fields of robotics, autonomous vehicles, and logistics are also presented.