Click on a search word OR use the drop-down choices to search for a paper.
2021
Singh, Neeraj Kumar; Lawford, Mark; Maibaum, Tom; Wassyng, Alan
A formal approach to rigorous development of critical systems Journal Article
In: Journal of Software: Evolution and Process, 2021.
Abstract | Links | BibTeX | Tags: certification, code generation, formal methods, proof‐based development, refinement, simulation, tabular expression, verification and validation
@article{Singh2021,
title = {A formal approach to rigorous development of critical systems},
author = {Neeraj Kumar Singh and Mark Lawford and Tom Maibaum and Alan Wassyng},
doi = { https://doi.org/10.1002/smr.2334},
year = {2021},
date = {2021-01-26},
urldate = {2021-01-26},
journal = {Journal of Software: Evolution and Process},
abstract = {Safety critical systems, such as medical, automotive, and avionics systems, play an important role in our daily lives. Increasing demand for new technologies in these safety critical systems requires rapid adoption of commercial hardware and software. However, the adoption of new hardware and software increases life‐threatening vulnerabilities. To aid in the reduction of these vulnerabilities and system failures, this paper proposes a framework based on formal methods for developing safety‐critical systems from requirements analysis to code generation. This framework includes a development process for documenting system requirements using tabular expressions, automatic formal model generation from the documented requirements, verification and validation of the generated formal models using proof techniques and animations, interactive simulation for validating the required behavior of the developed models by enabling domain experts to observe the system states according to, and finally, code generation from the formal model into a desired language. A prototype toolchain is developed to automate this framework. An assessment of the proposed framework is undertaken through a case study: insulin infusion pump (IIP).},
keywords = {certification, code generation, formal methods, proof‐based development, refinement, simulation, tabular expression, verification and validation},
pubstate = {published},
tppubtype = {article}
}
2015
Singh, Neeraj Kumar; Lawford, Mark; Maibaum, Thomas SE; Wassyng, Alan
Formalizing the Cardiac Pacemaker Resynchronization Therapy Proceedings Article
In: International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management, pp. 374–386, Springer International Publishing 2015.
BibTeX | Tags: event-B, formal methods, pacemaker, pacemaker resynchronization therapy, refinement, validation, verification
@inproceedings{singh2015formalizing,
title = {Formalizing the Cardiac Pacemaker Resynchronization Therapy},
author = {Singh, Neeraj Kumar and Lawford, Mark and Maibaum, Thomas SE and Wassyng, Alan},
year = {2015},
date = {2015-01-01},
booktitle = {International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management},
pages = {374--386},
organization = {Springer International Publishing},
keywords = {event-B, formal methods, pacemaker, pacemaker resynchronization therapy, refinement, validation, verification},
pubstate = {published},
tppubtype = {inproceedings}
}
Singh, Neeraj Kumar; Wang, Hao; Lawford, Mark; Maibaum, Thomas SE; Wassyng, Alan
Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements Proceedings Article
In: International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management, pp. 387–398, Springer International Publishing 2015.
BibTeX | Tags: event-B, formal methods, insulin infusion pump, refinement, validation, verification
@inproceedings{singh2015stepwise,
title = {Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements},
author = {Singh, Neeraj Kumar and Wang, Hao and Lawford, Mark and Maibaum, Thomas SE and Wassyng, Alan},
year = {2015},
date = {2015-01-01},
booktitle = {International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management},
pages = {387--398},
organization = {Springer International Publishing},
keywords = {event-B, formal methods, insulin infusion pump, refinement, validation, verification},
pubstate = {published},
tppubtype = {inproceedings}
}