Paper Info
Title
Towards a formal verification methodology for collective robotic systems
Abstract
We present a novel formal verification approach for collective robotic systems that is based on the use of the formal language Klaim and related analysis tools. While existing approaches focus on either micro- or macroscopic views of a system, we model aspects of both the robot hardware and behaviour, as well as relevant aspects of the environment. We illustrate our approach through a robotics scenario, in which three robots cooperate in a decentralized fashion to transport an object to a goal area. We first model the scenario in Klaim. Subsequently, we introduce random aspects to the model by stochastically specifying actions execution time. Unlike other approaches, the specification thus obtained enables quantitative analysis of crucial properties of the system. We validate our approach by comparing the results with those obtained through physics-based simulations.
Year
DOI
Venue
2012
10.1007/978-3-642-34281-3_7
Lecture Notes in Computer Science
Keywords
Field
DocType
model aspect,robotics scenario,related analysis tool,quantitative analysis,decentralized fashion,crucial property,actions execution time,collective robotic system,formal verification methodology,formal language,novel formal verification approach
Obstacle avoidance,Analysis tools,Robotic systems,Formal language,Computer science,Theoretical computer science,Artificial intelligence,Formal methods,Robot,Robotics,Distributed computing,Formal verification
Conference
Citations 
PageRank 
References 
8
0.49
15
Authors
8
Name
Order
Citations
PageRank
Edmond Gjondrekaj1151.09
Michele Loreti281258.60
rosario pugliese3144485.56
Francesco Tiezzi460446.24
Carlo Pinciroli541930.54
Manuele Brambilla632515.84
Mauro Birattari72021146.61
Marco Dorigo8140311211.61