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

Hi Matias,

I think that would be a great idea! It would have the added benefit that the protocol data types and structures could be used to generate header files so we could all have a true single information source for them (thinking of virtio_gen from crosvm/firecracker here).

Making a formal model part of the specification could allow generating some parts of the spec or at least validating the LaTeX itself against the model. On the other hand it might also raise the barrier to add new devices.

All in all, I'd be very interested to have a formal specification.



On 10.11.19 15:33, 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.

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