Software design of robot controllers with Petri nets: a case-study

Traditional techniques for designing complex real-time control software offer limited support for validating design before producing a final code. The need of early validation of the design of control software is increasing, due to the growing complexity of the software components and the strict timing requirements of run time control algorithms. The use of formal methods may greatly improve the design specification and validation processes. This paper presents a case-study that illustrates an approach for designing real-time control software with a specialized notation, formally defined by means of Petri nets. The formal approach is evaluated by comparison with a traditional approach based on the structured analysis