| dc.contributor.author | Shuja, Sana | |
| dc.description.abstract | Safety-critical medical devices play an important role in improving patients health and
lifestyle. Faulty behaviors of such devices can cause harm or even death. Often these faulty
behaviors are caused due to bugs in software programs used for digital control of the device. We
present a formal veri cation methodology that can be used to check the correctness of object
code programs that implement the safety-critical control functions of these medical devices. Our
methodology is based on the theory of Well-Founded Equivalence Bisimulation (WEB) re nement,
where both formal speci cations and implementations are treated as transition systems. First, we
present formal speci cation model for the medical device. Second, we develop correctness proof
obligations that can be applied to validate object code programs used in these devices. Formal
methods are not widely employed for the veri cation of safety critical medical devices. However,
using our methodology we were able to bridge the gap between two very important phases of
software life cycle: speci cation and veri cation. | en_US |
| dc.publisher | North Dakota State University | en_US |
| dc.rights | NDSU Policy 190.6.2 | |
| dc.title | Formal Verification Techniques for Safety Critical Medical Device Software Control | en_US |
| dc.type | Dissertation | en_US |
| dc.type | Video | en_US |
| dc.date.accessioned | 2016-07-11T14:27:48Z | |
| dc.date.available | 2016-07-11T14:27:48Z | |
| dc.date.issued | 2016 | |
| dc.identifier.uri | http://hdl.handle.net/10365/25736 | |
| dc.rights.uri | https://www.ndsu.edu/fileadmin/policy/190.pdf | |
| ndsu.degree | Doctor of Philosophy (PhD) | en_US |
| ndsu.college | Engineering | en_US |
| ndsu.department | Electrical and Computer Engineering | en_US |
| ndsu.program | Electrical and Computer Engineering | en_US |
| ndsu.advisor | Srinivasan, Sudarshan K. | |
