Advertisement

Formal Functional Verification of Device Drivers

  • Eyad Alkassar
  • Mark A. Hillebrand
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)

Abstract

We report on the formal functional verification of a simple device driver for an ATAPI hard disk in Isabelle/HOL. The proof is based on a functional model of the hard disk, which has been integrated into the instruction set architecture of a verified RISC processor as one of several memory-mapped devices. The result is an interleaved computational model, in which the devices and the processor take turns in execution. Even in this concurrent context, the verification can be kept largely sequential and modular with respect to the other devices. This is made possible by sound reordering of computation traces, given that devices do not interfere with each other and the driver monopolizes the hard disk. To the best of our knowledge, this paper presents the first formal functional verification of a device driver against a realistic device and system model.

Keywords

Hard Disk Execution Sequence Device Driver Memory Interface Hoare Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Hillebrand, M.A., Paul, W.: On the architecture of system verification environments. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 153–168. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  2. 2.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  3. 3.
    American National Standards Institute: ANSI NCITS 340-2000: AT Attachment-5 with Packet Interface (2000)Google Scholar
  4. 4.
    Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I/O devices in the context of pervasive system verification. In: ICCD 2005, pp. 309–316. IEEE Computer Society, Los Alamitos (2005)Google Scholar
  5. 5.
    Alkassar, E., et al.: Formal device and programming model for a serial interface. In: Beckert, B. (ed.) VERIFY 2007, pp. 4–20 (2007)Google Scholar
  6. 6.
    Berry, G., Kishinevsky, M., Singh, S.: System level design and verification using a synchronous language. In: ICCAD, pp. 433–440. IEEE Computer Society / ACM, Los Alamitos (2003)Google Scholar
  7. 7.
    Rashinkar, P., Paterson, P., Singh, L.: System-on-a-Chip Verification: Methodology and Techniques. Kluwer Academic Publishers, Norwell (2001)zbMATHGoogle Scholar
  8. 8.
    Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    Microsoft Corporation: SDV: Static driver verifier (2004), http://www.microsoft.com/whdc/devtools/tools/sdv.mspx
  10. 10.
    Hallgren, T., et al.: A principled approach to operating system construction in Haskell. In: Danvy, O., Pierce, B.C. (eds.) ICFP. ACM, New York (2005)Google Scholar
  11. 11.
    Heiser, G., et al.: Towards trustworthy computing systems: Taking microkernels to the next level. SIGOPS Oper. Syst. Rev. 41(4), 3–11 (2007)CrossRefGoogle Scholar
  12. 12.
  13. 13.
    Holzmann, G.J.: New challenges in model checking. In: Symposium on 25 years of Model Checking, Seattle, USA, LNCS, vol. 4925. Springer, Heidelberg (August 2006)Google Scholar
  14. 14.
    Freitas, L., Fu, Z., Woodcock, J.: POSIX file store in Z/Eves: An experiment in the verified software repository. In: ICECCS, pp. 3–14. IEEE Computer Society, Los Alamitos (2007)Google Scholar
  15. 15.
    Butterfield, A., Woodcock, J.: Formalising Flash memory: First steps. In: ICECCS, pp. 251–260. IEEE Computer Society, Los Alamitos (2007)Google Scholar
  16. 16.
    Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 317–331. Springer, Heidelberg (1998)Google Scholar
  18. 18.
    Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. 19.
    Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. Form. Methods Syst. Des. 28(3), 263–289 (2006)zbMATHCrossRefGoogle Scholar
  20. 20.
    Tverdyshev, S., Shadrin, A.: Formal verification of gate-level computer systems. In: Rozier, K.Y. (ed.) LFM 2008. NASA STI, NASA, pp. 56–58 (2008)Google Scholar
  21. 21.
    Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: ICFP 2004 (September 2004)Google Scholar
  22. 22.
    Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 109–123. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Leinenbach, D., Petrova, E.: Pervasive compiler verification – From verified programs to verified systems. In: SSV 2008. ENTCS, vol. 217, pp. 23–40. Elsevier Science B.V, Amsterdam (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Eyad Alkassar
    • 1
  • Mark A. Hillebrand
    • 2
  1. 1.Saarland UniversitySaarbrückenGermany
  2. 2.German Research Center for Artificial Intelligence (DFKI)SaarbrückenGermany

Personalised recommendations