| dc.contributor.author | Dubasi, Mohana Asha Latha | |
| dc.description.abstract | Real-time systems such as medical devices, surgical robots, and microprocessors are safety-critical
applications that have hard timing constraint. The correctness of real-time systems is
important as the failure may result in severe consequences such as loss of money, time and human
life. These real-time systems have software to control their behavior. Typically, this software
has source code which is converted to object code and then executed in safety-critical embedded
devices. Therefore, it is important to ensure that both source code and object code are error-free.
When dealing with safety-critical systems, formal verification techniques have laid the foundation
for ensuring software correctness.
Refinement based technique in formal verification can be used for the verification of real-time
interrupt-driven object code. This dissertation presents an automated tool that verifies the
functional and timing correctness of real-time interrupt-driven object code programs. The tool has
been developed in three stages. In the first stage, a novel timed refinement procedure that checks
for timing properties has been developed and applied on six case studies. The required model
and an abstraction technique were generated manually. The results indicate that the proposed
abstraction technique reduces the size of the implementation model by at least four orders of
magnitude. In the second stage, the proposed abstraction technique has been automated. This
technique has been applied to thirty different case studies. The results indicate that the automated
abstraction technique can easily reduce the model size, which would in turn significantly reduce
the verification time. In the final stage, two new automated algorithms are proposed which would
check the functional properties through safety and liveness. These algorithms were applied to the
same thirty case studies. The results indicate that the functional verification can be performed in
less than a second for the reduced model.
The benefits of automating the verification process for real-time interrupt-driven object code
include: 1) the overall size of the implementation model has reduced significantly; 2) the verification
is within a reasonable time; 3) can be applied multiple times in the system development process. | en_US |
| dc.publisher | North Dakota State University | en_US |
| dc.title | Timed Refinement for Verification of Real-Time Object Code Programs | en_US |
| dc.type | Dissertation | en_US |
| dc.type | Video | en_US |
| dc.date.accessioned | 2020-02-05T23:01:14Z | |
| dc.date.available | 2020-02-05T23:01:14Z | |
| dc.date.issued | 2018 | en_US |
| dc.identifier.uri | https://hdl.handle.net/10365/31372 | |
| dc.identifier.orcid | 0000-0003-1334-9263 | |
| dc.description.sponsorship | Several parts of this dissertation were funded by a grant from the United States Government and the generous support of the American people through the United States Department of State and the United States Agency for International Development (USAID) under the Pakistan – U.S. Science & Technology Cooperation Program. The contents do not necessarily reflect the views of the United States Government. | en_US |
| 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, Dr. Sudarshan K. | |
