M.D. Harrison, M. Drinnan, J.C. Campos, P. Masci, L. Freitas, C. di Maria and M. Whitaker
Safety analysis of software components of a dialysis machine using model checking
In Formal Aspects of Component Software, volume 10487 of Lecture Notes in Computer Science, pages 137-154. Springer. 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.

visit publisher   download PDF

@inproceedings{Harrison:2017,
 author = {M.D. Harrison and M. Drinnan and J.C. Campos and P. Masci and L. Freitas and C. di Maria and M. Whitaker},
 title = {Safety analysis of software components of a dialysis machine using model checking},
 booktitle = {Formal Aspects of Component Software},
 pages = {137-154},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 volume = {10487},
 year = {2017},
 doi = {10.1007/978-3-319-68034-7_8},
 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.},
 paperurl = {http://www.di.uminho.pt/~jfc/publications/HarrisonDCMFMW17-FACS-postprint.pdf}
}

Generated by mkBiblio 2.6.26