Complementary Verification of Embedded Software using ASD and Uppaal

Richard Doornbos, Jozef Hooman, and Bernard van Vlimmeren

Appeared in: Proceedings 8th International Conference on Innovations in Information Technology (IIT'12), pages 60-65, 2012.

ABSTRACT

To increase the confidence in the correctness of software components, we investigated the use of two complementary formal methods in industrial software development. We combine a commercial refinement checker, the ASD:Suite of the company Verum, with the academic verification tool Uppaal to encompass a larger range of verification possibilities. Wheras the ASD:Suite is based on the compositional verification of a single component with respect to its interface, Uppaal concentrates on the global verification of a closed system. Another difference is that ASD:Suite includes code generation from formal models, whereas Uppaal allows model simulation. The combination of the two tools has been applied in industry on a case study of a camera protection system.

pdf