Automatic software verification for robotics

Article type: Research Article

Authors: Mantovani, Jacopo

Affiliations: DIST – University of Genova, Viale F. Causa 13, 16145 Genova, Italy. Tel.: +39 010 3532150; Fax: +39 010 3532948; E-mail: jacopo.mantovani@unige.it

Abstract: This thesis investigates the application of novel software verification techniques to robotic systems. Control software lies at the core of these systems, and its complexity poses several challenges to the verification task, among which the intensive use of numeric values and constraints, and the manipulation of data structures. This thesis puts forward a Model Checking procedure specifically targeted for control software that manipulates numeric values, arithmetic constraints, and data structures such as arrays and matrices. It also demonstrates the effectiveness of this procedure in practice, when applied to robotic systems.

Keywords: Model Checking, software, robotics

DOI: 10.3233/AIC-2008-0426

Journal: AI Communications, vol. 21, no. 4, pp. 263-264, 2008