--- 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.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: John.Fitzgerald@ncl.ac.uk copyright_holders: [] corp_creators: [] creators_id: - ~ - ~ - John.Fitzgerald@ncl.ac.uk creators_name: - family: Macedo given: Hugo Daniel honourific: '' lineage: '' - family: Larsen given: Peter Gorm honourific: '' lineage: '' - family: Fitzgerald given: John honourific: '' lineage: '' data_type: ~ date: 2008 date_type: published datestamp: 2008-08-06 19:47:12 department: ~ dir: disk0/00/00/00/28 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 28 event_dates: '28-30 May, 2008' event_location: 'Turku, Finland' event_title: Formal Methods 2008 event_type: conference exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/28/1/pacemaker.pdf full_text_status: public funders: - EC - EPSRC (UK) id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-04-19 15:05:50 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://www.springerlink.com/content/5164786945751288/ output_media: ~ pagerange: 181-197 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: - FP 7 Deploy - TrAmS Platform Grant publication: ~ publisher: ~ refereed: TRUE 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.\r\n\r\n2. 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.\r\n\r\n3. Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object–oriented Systems. Springer, New York (2005)\r\n\r\n4. 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.\r\n\r\n5. 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\r\n\r\n6. 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\r\n\r\n7. CSK: Development Guidelines for Real Time Systems using VDMTools. Technical report, CSK Systems (2008)\r\n\r\n8. Boston Scientific: Pacemaker system specification. Technical report, Boston Scientific (January\r\n2007) http://www.cas.mcmaster.ca/sqrl/SQRLDocuments/PACEMAKER.pdf.\r\n\r\n9. Woodcock, J.: First Steps in the Verified Software Grand Challenge. Computer 39(10) (2006) 57–64\r\n\r\n10. Ellenbogen, K.A., Wood, M.A.: Cardiac Pacing and ICDs. 4th edn. Blackwell (2005)\r\n\r\n11. 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.\r\n\r\n12. 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)\r\n\r\n13. Overture Group: The VDM Portal. http://www.vdmportal.org (2007)\r\n\r\n14. Lano, K.: Logic specification of reactive and real-time systems. Journal of Logic and Computation 8(5) (1998) 679–711\r\n\r\n15. 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/.\r\n\r\n16. CSK: VDMTools homepage. http://www.vdmtools.jp/en/ (2007)\r\n\r\n17. 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).\r\n\r\n18. Macedo, H.: Validating and Understanding Boston Scientific Pacemaker Requirements.\r\n\r\nMaster’s thesis, Minho University, Portugal (October 2007)\r\n19. Macedo, H.: VDM models of the Pacemaker Challenge (2007)\r\nhttp://www.vdmportal.org/twiki/bin/view/Main/PacemakerCaseStudy.\r\n\r\n20. 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)\r\n\r\n21. Verhoef, M.: Modeling and Validation Distributed Embedded Real-Time Systems. PhD thesis, Radboud University Nijmegen (2008)\r\n\r\n22. 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)\r\n\r\n23. de Boer, F.: CREDO: Modeling and analysis of evolutionary structures for distributed services (2007) http://www.cwi.nl/projects/credo/.\r\n\r\n24. Lecomte, T.: Event B Reference Manual. Technical report, MATISSE/ClearSy (2001)\r\n\r\n25. 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\r\n\r\n26. Douglas, B.P.: Real Time UML – Advances in the UML for real-time systems. Third edn. Addison-Wesley (2004)\r\n\r\n27. 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)\r\n\r\n28. 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)\r\n\r\n29. 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\r\n\r\n30. 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\r\n\r\n31. 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\r\n\r\n32. 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\r\n\r\n33. Vermolen, S.: Automatically Discharging VDM Proof Obligations using HOL. Master’s thesis, Radboud University Nijmegen, Computer Science Department (August 2007)" related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 32 series: ~ skill_areas: [] source: ~ status_changed: 2008-08-06 19:47:12 subjects: - deploy_tooldev - deploy_method succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System using VDM type: conference_item userid: 11 volume: ~