Industrial Experiences with Formal Verification

Jozef Hooman

Embedded Systems Institute, Eindhoven & Radboud University Nijmegen

The product ASD:Suite of the Dutch company Verum provides a modeling approach which combines compositional model checking and code generation. We discuss experiences with this tool for the design of interventional X-ray systems at Philips Healthcare. This concerns formal interface definitions between the main system components and detailed design of control components. In addition, we present a case study at FEI Company, a manufacturer of electron microscopes. This concerns the combination of ASD:Suite with the Uppaal model checker to encompass a larger range of verification possibilities, in response to a request by industrial software developers. We derived the essential models from a camera protection system, translated them to Uppaal and - by verifying required properties - found some small design errors.