M.D. Harrison, L. Freitas, M. Drinnan, J.C. Campos, P. Masci, C. di Maria and M. Whitaker
Formal Techniques in the Safety Analysis of Software Components of a new Dialysis Machine
Science of Computer Programming, 175:17-34, April. 2019.

Abstract

The paper is concerned with the practical use of formal techniques to contribute to the risk analysis of a new neonatal dialysis machine. The described formal analysis focuses on the controller component of the software implementation. The controller drives the dialysis cycle and deals with error management. The logic was analysed using model checking techniques and the source code was analysed formally, checking type correctness conditions, use of pointers and shared memory. The analysis provided evidence of the verification of risk control measures relating to the software component. The productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and the analyst using the formal analysis tools, provided a basis for the development of rationale for the effectiveness of the evidence.

visit publisher   visit publisher  

@article{Harrison:2019,
 author = {M.D. Harrison and L. Freitas and M. Drinnan and J.C. Campos and P. Masci and C. di Maria and M. Whitaker},
 journal = {Science of Computer Programming},
 title = {Formal Techniques in the Safety Analysis of Software Components of a new Dialysis Machine},
  volume = {175},
 pages = {17-34},
 month = {April},
 year = {2019},
 doi = {10.1016/j.scico.2019.02.003},
 hdl ={1822/66934},
 abstract = {The paper is concerned with the practical use of formal techniques to contribute to the risk analysis of a new neonatal dialysis machine. The described formal analysis focuses on the controller component of the software implementation. The controller drives the dialysis cycle and deals with error management. The logic was analysed using model checking techniques and the source code was analysed formally, checking type correctness conditions, use of pointers and shared memory. The analysis provided evidence of the verification of risk control measures relating to the software component. The productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and the analyst using the formal analysis tools, provided a basis for the development of rationale for the effectiveness of the evidence.},
  keywords = {_ivy}
}

Generated by mkBiblio 2.6.26