[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]
Subject: Re: Formal specification of virtIO
Hello, I am investigating the possibility to use a higher-level language to describe virtio concepts. I am writing down this research at https://github.com/MatiasVara/virtioml. I defined a metamodel that captures concepts and relationships between these concepts. I also built a simple transformation to generate the headers in C. This transformation may be extended to other languages. I am currently investigating the possibility to model the VIRTIO_CONFIG_S_* status register state machine to verify that a virtio driver follows the specification. To do this, I am first using a formalism to encode the specification, and from that code, I generate the instrumentation code that goes in the driver. The instrumentation code warns when the specification is violated. This is, however, a very draft work. Regards, Matias. On Sun, Nov 10, 2019 at 03:33:20PM +0100, Matias Vara wrote: > Hello everyone, > > I have started to think of the formalization of the virtIO specification. > Roughly speaking, I could use a formal language to "code" the virtIO spec. > As far as I can think, this has three benefits: > 1. You can validate any implementation. > 2. You can generate the implementation for a given target. For example, you > could be able to generate the implementation of a virtIO device in VHDL. > 3. You can provide simulation and verification before any implementation. > In automotive, this is interesting because you ease the certification so > formalization pays off. > > Do you think this may be interesting work to do to become the virtIO > specification more robust? > > Regards, Matias.