\input zb-basic \input zb-ioport \iteman{io-port 06103238} \itemau{Osaiweran, Ammar; Fransen, Tom; Groote, Jan Friso; van Rijnsoever, Bart} \itemti{Experience report on designing and developing control components using formal methods.} \itemso{Giannakopoulou, Dimitra (ed.) et al., FM 2012: Formal methods. 18th international symposium, Paris, France, August 27--31, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32758-2/pbk). Lecture Notes in Computer Science 7436, 341-355 (2012).} \itemab Summary: This paper reports on experiences from an industrial project related to developing control components of an interventional X-ray system, using formal techniques supplied by the Analytical Software Design approach, of the company Verum. We illustrate how these formal techniques were tightly integrated with the standard development processes and the steps accomplished to obtain verifiable components using model checking. Finally, we show that applying these formal techniques could result in quality software and we provide supporting statistical data for this regard. \itemrv{~} \itemcc{} \itemut{formal methods in industry; analytical software design} \itemli{doi:10.1007/978-3-642-32759-9\_29} \end