Learning middleware models for verification of distributed control programs

Our proposal is to ease the application of automated verification techniques by identifying abstract middleware models in the form of finite-state automata. The identification procedure is itself largely automated, and the only prerequisite is for the middleware to be available for controlled experimentation. Once middleware models are computed, behaviors that would lead to unsafe operation can be spotted automatically on a composition of identified middleware and control software models using model checking techniques. The approach is based on our tool AIDE - Automata IDentification Engine - to identify abstract middleware models, and the model checker SPIN to verify control units. To validate our approach, we consider four different case studies built on YARP publish-subscribe middleware. Our results confirm that AIDE enables the extension of precise engineering methods to distributed control software in robotics.