Verifying the Conformance of a Driver Implementation to the VirtIO Specification
Matias Vara Larsen
Huawei Research Center Grenoble, France
matias.vara.larsen@huawei.com
ABSTRACT
VIRTIO is a specification that enables developers to base on a common interface to implement devices and drivers for virtual environments. This paper proposes the verification and analysis of the VIRTIO specification by using the Clock Constraint Specification Language (CCSL) [1]. In our proof-ofconcept approach, a verification engineer translates requirements into a CCSL specification. Then, the tool TIMESQUARE [2] is used to detect inconsistencies with a implementation but also to understand what the specification enables. This paper aims to present the approach and to have face-to-face discussions and debate about the benefits, drawbacks and trade-offs.
Keywords: Kernel, Virtio, Conformance, Verification, Formal.
