Re: Formal specification of virtIO

[Matias Ezequiel Vara Larsen <matiasevara@gmail.com>]

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.