Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/5444
Title: Safety Analysis of Software Components of a Dialysis Machine Using Model Checking
Authors: Harrison,MD
Drinnan,M
José Creissac Campos
Paolo Masci
Freitas,L
Maria,Cd
Whitaker,M
Issue Date: 2017
Abstract: The paper describes the practical use of a model checking technique to contribute to the risk analysis of a new paediatric dialysis machine. The formal analysis focuses on one component of the system, namely the table-driven software controller which drives the dialysis cycle and deals with error management. The analysis provided evidence of the verification of risk control measures relating to the software component. The paper describes the productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and an analyst who had experience of using the formal analysis tools. There were two aspects to this dialogue. The first concerned the translation of safety requirements so that they preserved the meaning of the requirement. The second involved understanding the relationship between the software component under analysis and the broader concern of the system as a whole. The paper focuses on the process, highlighting how the team recognised the advantages over a more traditional testing approach. © 2017, Springer International Publishing AG.
URI: http://repositorio.inesctec.pt/handle/123456789/5444
http://dx.doi.org/10.1007/978-3-319-68034-7_8
metadata.dc.type: conferenceObject
Publication
Appears in Collections:HASLab - Articles in International Conferences

Files in This Item:
File Description SizeFormat 
P-00N-18G.pdf740.9 kBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.