Rigorous Model-based Development of Programmable Electronic Medical Systems (PEMS): from Requirements to Code

Programmable Electronic Medical Systems (PEMS) are safety-critical system. They have effects on people health and, in case of malfunctions, they can seriously compromise human safety. For this reason, the software installed on these devices must be guaranteed through rigorous processes to assure safety and reliability. Moreover, correct operation of a medical device depends upon the controlling software, whose development should adhere to certification standards. The rigorous process presented in this thesis is based on the Abstract State Machines (ASMs) formal method, a mathematically based technique for the specification, analysis and development of software systems. The ASM formal approach proposes an incremental life cycle model for software development based on model refinement. It covers the main software engineering activities (specification, validation, verification, conformance checking), and it is supported by a wide range of tools which are part of the Asmeta (ASM mETAmodeling) framework. In this thesis, the ASM development approach and its supporting Asmeta framework are used to propose a rigorous development process for PEMS. The final goal is to provide a process able to guarantee the development of correct and controllable systems in a correct and controllable way. The definition of this process has leaded to some improvements of the method, mainly regarding the textual and graphical notations, and the automatic code generation from models. A new rigorous notation, Unified Syntax for Abstract State Machine (UASM), has been defined to provide a stable language kernel for ASMs. Formal models are not widely used in practice, since they are considered difficult to develop and understand. For this reason, we here make a proposal of a tool for a graphical representation of ASM models in order to increase the readability. Moreover, we have devised a methodology to generate the desired source code from ASM models. The tool automatically translates the formal specification into the target code (C++ for Arduino in the present case) and it keeps true the system behavior and the properties verified during validation and verification. The hemodialysis machine and the stereoacuity test are used as real case studies to show the applicability and effectiveness of the ASM-based development process in the area of PEMS.