OASIS Mailing List ArchivesView the OASIS mailing list archive below
or browse/search using MarkMail.


Help: OASIS Mailing Lists Help | MarkMail Help

virtio-comment message

[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]

Subject: Re: [virtio-comment] Formal specification of virtIO

On Sun, Nov 10, 2019 at 03:33:20PM +0100, Matias Vara wrote:
> 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?

As a starting point you could propose a formal model of an aspect of the
specification, like the device lifecycle VIRTIO_CONFIG_S_* status
register state machine (start easy!).

It would already offer the advantages you mentioned for a subset of the
specification and give the community a chance to get familiar with the
tools and workflow.

Even if it turns out to be impractical to formalize the entire VIRTIO
specification, it will certainly reveal things that can be improved in
the current spec.


Attachment: signature.asc
Description: PGP signature

[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]