Using the Time Petri Nets Formalism for Specificaction, Validation and Code Generation in Robot-Control Applications

The main objective of this paper is to show the advantages of using the time Petri net formalism for specification, validation, and code generation in robot-control applications. To achieve this objective, we consider as application the development of a control system for a mobile robot with a rotating rangefinder laser sensor with two degrees of freedom to be used in navigation tasks with obstacle avoidance. It is shown how the use of the time Petri net formalism in the whole development cycle can fulfill the reliability requirement of real-time systems, make the system development easy and quick, strongly reduce the time for the testing and tuning phases and, therefore, reduce the development cost significantly. It allows verification of functional and temporal requirements, error detection in the early stages of the development cycle, and automatic code generation, avoiding coding mistakes. Experimental tests show that the theoretical results obtained from the analysis of formal system models match the real-time behavior of the robotic system