Complementary verification of embedded software using ASD and Uppaal

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.