Abstract
We present an efficient approach to reachability analysis of Büchi Pushdown System (BPDS) models for Hardware/Software (HW/SW) co-verificat-ion. This approach utilizes the asynchronous nature of the HW/SW interactions to reduce unnecessary HW/SW state transition orders being explored in co-verificat-ion. The reduction is applied when the verification model is constructed. We have realized this approach in our co-verification tool, CoVer, and applied it to the co-verification of two fully functional Windows device drivers with their device models respectively. Both of the drivers are open source and their original C code has been used. CoVer has proven seven safety properties and detected seven previously undiscovered software bugs. Evaluation shows that the reduction can significantly scale co-verification.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Li, J., Xie, F., Ball, T., Levin, V., McGarvey, C.: An automata-theoretic approach to hardware/software co-verification. In: Proc. of FASE (2010)
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis (2002)
Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 345. Springer, Heidelberg (1998)
Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Proc. of EuroSys (2006)
Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenigün, H.: Combining software and hardware verification techniques. FMSD (2002)
Xie, F., Yang, G., Song, X.: Component-based hardware/software co-verification for building trustworthy embedded systems. JSS 80(5) (2007)
Monniaux, D.: Verification of device drivers and intelligent controllers: a case study. In: Proc. of EMSOFT (2007)
Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. (2000)
A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, Springer, Heidelberg (1997)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. PhD thesis (1994)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)
Microsoft: Synchronizing interrupt code. In: MSDN (2009), msdn.microsoft.com/en-us/library/aa490313.aspx
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, J., Xie, F., Ball, T., Levin, V. (2010). Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification. In: Touili, T., Cook, B., Jackson, P. (eds) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science, vol 6174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14295-6_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-14295-6_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14294-9
Online ISBN: 978-3-642-14295-6
eBook Packages: Computer ScienceComputer Science (R0)