Title :
Dealing with I/O devices in the context of pervasive system verification
Author :
Hillebrand, Mark A. ; der Rieden, Thomas In ; Paul, W.J.
Author_Institution :
Dept. of Comput. Sci., Saarland Univ., Saarbruken, Germany
Abstract :
Device drivers can be tested and debugged much better with techniques from the field of formal verification than with classical methods. The total verification of drivers together with the underlying hardware, however has remained an unsolved problem. Here we outline a paper-and-pencil solution for this problem and report on the status of the formal verification. This work is part of the Verisoft project. In its subproject 2, the seamless verification of the academic system, comprising hardware, system software and applications, is attempted. We survey the techniques and tools used for program verification in Verisoft.
Keywords :
formal verification; program assemblers; program debugging; ubiquitous computing; I-O devices; Verisoft project; device driver verification; formal verification; paper-and-pencil solution; pervasive system verification; program verification; seamless verification; system software; Application software; Assembly; Computer languages; Computer science; File systems; Formal verification; Hardware; High level languages; System software; Testing;
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 2005. ICCD 2005. Proceedings. 2005 IEEE International Conference on
Print_ISBN :
0-7695-2451-6
DOI :
10.1109/ICCD.2005.42