Abstract
This paper describes the use of a formal method to support component-based development in the healthcare domain. The method is based on a commercial tool suite which combines formal modeling, compositional model checking, and code generation. The main approach of the tool suite will be explained and demonstrated from a user point of view. We report about experiences with this approach at the company Philips Healthcare for the design of control software for advanced interventional X-ray systems. This concerns formal interface definitions between the main system components and detailed design of control components.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)
Booch, G., Rumbaugh, J.E., Jacobson, I.: The unified modeling language user guide - the ultimate tutorial to the UML from the original designers. Addison-Wesley object technology series. Addison-Wesley-Longman (1999)
Broadfoot, G.H., Broadfoot, P.J.: Academia and industry meet: Some experiences of formal methods in practice. In: 10th Asia-Pacific Software Engineering Conferenc (APSEC 2003), pp. 49–58 (2003)
ClearSy: Atelier B, industrial tool supporting the B method (2011), http://www.atelierb.eu/en/
CSK Systems Corporation: VDMTools, industrial tool supporting VDM++ (2011), http://www.vdmtools.jp/en/
Esterel Technologies: SCADE Suite, model based development environment dedicated to critical embedded software (2011), http://www.esterel-technologies.com/products/scade-suite/
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-oriented Systems. Springer, New York (2005), http://www.vdmbook.com
Formal Systems (Europe) Ltd: FDR2 model checker (2011), http://www.fsel.com/
Groote, J.F., Osaiweran, A., Wesselius, J.H.: Analyzing the effects of formal methods on the development of industrial control software. In: Proceedings of the IEEE ICSM 2011, pp. 467–472 (2011)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
Hooman, J.: Specification and Compositional Verification of Real-Time Systems. LNCS, vol. 558. Springer, Heidelberg (1991)
Hopcroft, P.J., Broadfoot, G.H.: Combining the box structure development method and CSP for software development. Electronic Notes in Theoretical Computer Science 128(6), 127–144 (2005)
Meyer, B.: Applying “design by contract”. IEEE Computer 25(10), 40–51 (1992)
Mills, H.D.: Stepwise refinement and verification in box-structured systems. Computer 21, 23–36 (1988)
Prowell, S.J., Poore, J.H.: Foundations of sequence-based software specification. IEEE Transactions on Software Engineering 29, 417–429 (2003)
Roscoe, A.W.: The theory and practice of concurrency. Prentice Hall (1998)
Verum: ASD:Suite (2011), http://www.verum.com/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hooman, J., Huis in ’t Veld, R., Schuts, M. (2012). Experiences with a Compositional Model Checker in the Healthcare Domain. In: Liu, Z., Wassyng, A. (eds) Foundations of Health Informatics Engineering and Systems. FHIES 2011. Lecture Notes in Computer Science, vol 7151. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32355-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-32355-3_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32354-6
Online ISBN: 978-3-642-32355-3
eBook Packages: Computer ScienceComputer Science (R0)