creators_name: Macedo, Hugo Daniel creators_name: Larsen, Peter Gorm creators_name: Fitzgerald, John creators_id: John.Fitzgerald@ncl.ac.uk type: conference_item datestamp: 2008-08-06 19:47:12 lastmod: 2010-04-19 15:05:50 metadata_visibility: show title: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System using VDM ispublished: pub subjects: deploy_tooldev subjects: deploy_method full_text_status: public pres_type: paper abstract: The construction of formal models of real-time distributed systems is a considerable practical challenge. We propose and illustrate a pragmatic incremental approach in which detail is progressively added to abstract system-level specifications of functional and timing properties via intermediate models that express system architecture, concurrency and timing behaviour. The approach is illustrated by developing a new formal model of the cardiac pacemaker system proposed as a “grand challenge” problem in 2007. The models are expressed using the Vienna Development Method (VDM) and are validated primarily by scenario-based tests, including the analysis of timed traces. We argue that the insight gained using this staged modelling approach will be valuable in the subsequent development of implementations, and in detecting potential bottlenecks within suggested implementation architectures. date: 2008 date_type: published pagerange: 181-197 event_title: Formal Methods 2008 event_location: Turku, Finland event_dates: 28-30 May, 2008 event_type: conference refereed: TRUE official_url: http://www.springerlink.com/content/5164786945751288/ referencetext: 1. Jones, C.B.: Systematic Software Development Using VDM. Second edn. Prentice-Hall International, Englewood Cliffs, New Jersey (1990) ISBN 0-13-880733-7. 2. Fitzgerald, J., Larsen, P.G.: Modelling Systems – Practical Tools and Techniques in Software Development. Cambridge University Press, The Edinburgh Building, Cambridge CB2 2RU, UK (1998) ISBN 0-521-62348-0. 3. Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object–oriented Systems. Springer, New York (2005) 4. Fitzgerald, J.S., Larsen, P.G.: Triumphs and Challenges for the Industrial Application of Model-Oriented Formal Methods. In Margaria, T., Philippou, A., Steffen, B., eds.: Proc.2nd Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2007). (2007) Also Technical Report CS-TR-999, School of Computing Science, Newcastle University. 5. Verhoef, M., Larsen, P.G., Hooman, J.: Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In Misra, J., Nipkow, T., Sekerinski, E., eds.: FM 2006: Formal Methods, Lecture Notes in Computer Science 4085 (2006) 147–162 6. Fitzgerald, J.S., Larsen, P.G., Tjell, S., Verhoef, M.: Validation Support for Real-Time Embedded Systems in VDM++. In Cukic, B., Dong, J., eds.: Proc. HASE 2007: 10th IEEE High Assurance Systems Engineering Symposium, IEEE (November 2007) 331–340 7. CSK: Development Guidelines for Real Time Systems using VDMTools. Technical report, CSK Systems (2008) 8. Boston Scientific: Pacemaker system specification. Technical report, Boston Scientific (January 2007) http://www.cas.mcmaster.ca/sqrl/SQRLDocuments/PACEMAKER.pdf. 9. Woodcock, J.: First Steps in the Verified Software Grand Challenge. Computer 39(10) (2006) 57–64 10. Ellenbogen, K.A., Wood, M.A.: Cardiac Pacing and ICDs. 4th edn. Blackwell (2005) 11. Mukherjee, P., Bousquet, F., Delabre, J., Paynter, S., Larsen, P.G.: Exploring Timing Properties Using VDM++ on an Industrial Application. In Bicarregui, J., Fitzgerald, J., eds.: Proceedings of the Second VDM Workshop. (September 2000) Available at www.vdmportal.org. 12. Larsen, P.G., Hansen, B.S., et al.: Information technology – Programming languages, their environments and system software interfaces – Vienna Development Method – Specification Language – Part 1: Base language (December 1996) 13. Overture Group: The VDM Portal. http://www.vdmportal.org (2007) 14. Lano, K.: Logic specification of reactive and real-time systems. Journal of Logic and Computation 8(5) (1998) 679–711 15. Verhoef, M., Larsen, P.G.: Interpreting Distributed System Architectures Using VDM++ – A Case Study. In Sauser, B., Muller, G., eds.: 5th Annual Conference on Systems Engineering Research. (March 2007) Available at http://www.stevens.edu/engineering/cser/. 16. CSK: VDMTools homepage. http://www.vdmtools.jp/en/ (2007) 17. Kurita, T., Oota, T., Nakatsugawa, Y.: Formal specification of an embedded IC for cellular phones. In: Proceedings of Software Symposium 2005, Software Engineers Associates of Japan (June 2005) 73–80 (in Japanese). 18. Macedo, H.: Validating and Understanding Boston Scientific Pacemaker Requirements. Master’s thesis, Minho University, Portugal (October 2007) 19. Macedo, H.: VDM models of the Pacemaker Challenge (2007) http://www.vdmportal.org/twiki/bin/view/Main/PacemakerCaseStudy. 20. Sørensen, R.A., Nygaard, J.M.: Evaluating Distributed Architectures using VDM++ Real- Time Modelling with a Proof of Concept Implementation. Master’s thesis, Enginering College of Aarhus (December 2007) 21. Verhoef, M.: Modeling and Validation Distributed Embedded Real-Time Systems. PhD thesis, Radboud University Nijmegen (2008) 22. Vilas, A.F., Arias, J.J.P., Redondo, R.P.D., Martinez, A.B.B.: Formalizing Incremental Design in Real-time Area: SCTL/MUS-T. In: Proceedings of the 26 th Annual International Computer Software and Applications Conference (COMPSAC02), IEEE (2002) 23. de Boer, F.: CREDO: Modeling and analysis of evolutionary structures for distributed services (2007) http://www.cwi.nl/projects/credo/. 24. Lecomte, T.: Event B Reference Manual. Technical report, MATISSE/ClearSy (2001) 25. Suhaib, S.M., Mathaikutty, D.A., Shukla, S.K., Berner, D.: XFM: An Incremental Methodology for Developing Formal Models. ACM Transactions on Design Automation of Electronic Systems 10(4) (October 2005) 589–609 26. Douglas, B.P.: Real Time UML – Advances in the UML for real-time systems. Third edn. Addison-Wesley (2004) 27. de Jong, G.: A UML-Based Design Methodology for Real-Time and Embedded Systems. In: Proceedings of the 2002 Design, Automation and Test in Europe Conference and Exhibition (DATE.02), IEEE (2002) 28. Burmester, S., Giese, H., Hirsch, M., Schilling, D.: Incremental Design and Formal Verification with UML/RT in the FUJABA Real-Time Tool Suite. In: Proceedings of the International Workshop on Specification and validation of UML models for Real Time and embedded Systems, SVERTS2004, UML2004 (2004) 29. Uchitel, S., Kramer, J., Magee, J.: Incremental Elaboration of Scenario-Based Specifications and Behavior Models Using Implied Scenarios. ACM Transactions on Software Engineering and Methodology 13(1) (January 2004) 37–85 30. Jing Liu, J.D., Lutz, R.: Safety analysis of software product lines using state-based modeling. Journal of Systems and Software 80(11) (November 2007) 1879–1892 31. Verhoef, M., Visser, P., Hooman, J., Broenink, J.: Co-simulation of Real-time Embedded Control Systems. In Davies, J., Gibbons, J., eds.: Integrated Formal Methods: Proc. 6th. Intl. Conference. Lecture Notes in Computer Science 4591, Springer-Verlag (July 2007) 639–658 32. Andrews, Z.H., Fitzgerald, J.S., Verhoef, M.: Resilience Modelling through Discrete Event and Continuous Time Co-Simulation. In: Proc. 37th Annual IFIP/IEEE Intl. Conf. on Dependable Systems and Networks (Supp. Volume), IEEE Computer Society (June 2007) 350–351 33. Vermolen, S.: Automatically Discharging VDM Proof Obligations using HOL. Master’s thesis, Radboud University Nijmegen, Computer Science Department (August 2007) citation: Macedo, Hugo Daniel and Larsen, Peter Gorm and Fitzgerald, John (2008) Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System using VDM. In: Formal Methods 2008, 28-30 May, 2008, Turku, Finland. document_url: http://deploy-eprints.ecs.soton.ac.uk/28/1/pacemaker.pdf