Environment Modeling of Linux Operating System Device Drivers
Abstract
In static device driver verification of Linux operating system it is necessary to take into account the specifics of the communication between drivers and kernel core as far as it plays the main role in the drivers’ behavior. At the same time the verification of a driver together with kernel core source code is not feasible due to complexity and size of the resulting source code. As a solution the paper presents the modeling method of driver environment based on R.Milner calculus and the method of model translation into C program. Being linked with the driver the resulting program has the same scenarios of driver behavior as the real driver environment in operating system from the static verification tools point of view.
About the Authors
I. S. Zakharov
ISP RAS, Moscow
Russian Federation
Russian Federation
V. S. Mutilin
ISP RAS, Moscow
Russian Federation
Russian Federation
E. M. Novikov
ISP RAS, Moscow
Russian Federation
Russian Federation
A. V. Khoroshilov
ISP RAS, Moscow
Russian Federation
Russian Federation
References
1. Beyer D. Second Competition on Software Verification. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7795, pp. 594-609, 2013. doi: 10.1007/978-3-642-36742-7_43
2. Beyer D., Henzinger T., Jhala R., Majumdar R. The Software Model Checker Blast: Applications to Software Engineering. International Journal on Software Tools for Technology Transfer (STTT), vol. 5, pp. 505-525, 2007. doi: 10.1007/s10009-007-0044-z
3. Shved P., Mandrykin M., Mutilin V. Predicate Analysis with Blast 2.7. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 525–527, 2012. doi: 10.1007/978-3-642-28756-5_39
4. Beyer D., Keremoglu M.E. CPAchecker: A Tool for Configurable Software Verification. In Proc. Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 184–190, 2011. 10.1007/978-3-642-22110-1_16
5. Milner R. The Polyadic π-Calculus: a Tutorial. In Proc. Logic and Algebra of Specification, NATO ASI Series, vol. 94, pp 203-246, 1993. doi: 10.1007/978-3-642-58041-3_6
6. Mutilin V.S. Verifikatsiya drajverov operatsionnoj sistemy Linux pri pomoshhi predikatnykh abstraktsij [Linux drivers verification with help of predicate abstractions]. Dissertatsiya na soiskanie uchenoj stepeni k.f.-m.n. [PhD thesis], 2012 (in Russian).
7. Mandrykin M.U., Mutilin V.S., Novikov E.M., Khoroshilov А.V., Shved P.E. Using linux device drivers for static verification tools benchmarking. Programming and Computer Software, vol. 35, issue 5, pp. 245-256, 2012. doi: 10.1134/S0361768812050039
8. Mutilin V.S., Novikov E.M., Strakh А.V., Khoroshilov А.V., Shved P.E. Аrkhitektura Linux Driver Verification [Linux Driver Verification Architecture]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 20, pp. 163-187, 2011 (in Russian).
9. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an Open Framework for C Verification Tools Benchmarking. In Proc. Perspectives of Systems Informatics (PSI), LNCS, vol 7162, pp. 82-91, 2012. doi: 10.1007/978-3-642-29709-0_17
Review
For citations:
Zakharov I.S., Mutilin V.S., Novikov E.M., Khoroshilov A.V. Environment Modeling of Linux Operating System Device Drivers. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2013;25:85-112. (In Russ.)
Email this article 