Visual Specification of Properties for Robotic Designs

• Waldeck Lindoso Jr. UFRPE
• Sidney C. Nogueira UFRPE
• Renato Domingues UFRPE
• Lucas Lima UFRPE

Resumo

RoboChart is a diagrammatic notation based on UML designed for modelling robotic software that has well-defined semantics in the notation of CSP process algebra, enabling the automatic proof of process refinements using the FDR tool. Although RoboChart allows the specification of the robot software, the definition of application-specific properties of RoboChart models must be specified using the CSP notation. Thus, the designer must be familiar with CSP to define and verify properties. This work proposes an approach for the automatic verification of properties using a diagrammatic notation that expresses the behaviour of RoboChart models. The approach proposes a diagrammatic notation based on UML activity diagrams that support the specification of behaviour mixing standard elements of the activity diagram with elements of RoboChart as events and operations. The diagram behaviour is formalised as a CSP process used to verify the properties of a RoboChart component. A plug-in for the Astah modelling tool has been developed to translate the diagram to CSP and call the FDR refinement checker, which verifies whether the RoboChart model refines the property specified with the proposed notation. Our proposed approach allows the designer to specify and verify properties of RoboChart models using diagrammatic notations with no knowledge of the underlying formal semantics.

Palavras-chave: RoboChart properties, Activity diagram, Astah, CSP, FDR