Many high-integrity software development processes prevent any assumptions about the system hardware, but this makes it impossible to use these techniques on software that must interact with the hardware, such as device drivers. This work takes the opposite approach: if the analyst accepts that the analysis will only be valid for a particular target system then the specification of the system can be used to infer the behaviour of the software that interacts with it. An analysis process is developed that operates on disassembled executable files and formal specifications of the target platform to produce CSP-OZ formal models of the software’s behaviour. This analysis process is implemented in a prototype called Spurinna. This is demonstrated in conjunction with the verification tools Z2SAL and the SAL suite to demonstrate the verification of properties of an example program.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Taylor12,
author = {Ramsay Taylor},
editor = {John Derrick and
John S. Fitzgerald and
Stefania Gnesi and
Sarfraz Khurshid and
Michael Leuschel and
Steve Reeves and
Elvinia Riccobene},
title = {Verification of Hardware Interaction Properties of Software},
booktitle = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7316},
pages = {308--322},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-30885-7\_22},
doi = {10.1007/978-3-642-30885-7\_22},
timestamp = {Sun, 02 Jun 2019 21:23:59 +0200},
biburl = {https://dblp.org/rec/conf/asm/Taylor12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}