On the 10th of March 2016 at 23:21, Wolfgang Keller wrote
Interesting statement on the Muen kernel section: "The world’s first Open
Source microkernel that has been formally proven to contain no runtime errors at the
source code level. “
We proved full functional correctness (which is a superset of absence of
runtime errors) for seL4 in 2009. I must be missing something.
I believe how it is meant is the following: "The first kernel to both
reach being open source and being proven to contain no runtime errors
is Muen." (of course among the kernels that are *now* open source,
seL4 is the first one for which the absence of runtime errors was
proven)
Wolfgang
Indeed, I also found this statement a little confusing at first.
But nevertheless, I am still very critical with this claim by NICTA as
well, because I am virtually for 100% sure, that on the one hand the
NASA verified an RTOS for a spacecraft, the USArmy (DARPA, AFRL, etc.)
verified an RTOS for a cruise missile or another critical equipement,
and one of the largest aircraft manufacturers (e.g. Boeing, Lockheed
Martin, Tupolev, or Mikoyan-Gurevich) verified some kind of a small
operating system.
On the other hand there were always attempts to do such a work, as it
could be seen for example with [1], and it is hardly not convincing that
in the following 22 years nobody else tried and eventually achieved it.
In the case of the NASA and the USArmy I am still waiting for a
disclosure of historical informations, which in the case of the army
most potentially is still confidential.
What makes a judgement even more difficult or even impossible is the
problem to draw the exact limits in relation with what is understood as
a microkernel, a general purpose operating system kernel and so on for
being able to make such a statement "The first verified ... system" at all.
Regards
Christian Stroetmann
[1] William R. Bevier: "A Verified Operating System Kernel", Technical
Report 11, October, 1987
On Thu, Mar 10, 2016 at 10:33 PM, Gernot Heiser<[email protected]> wrote:
Interesting statement on the Muen kernel section: "The world’s first Open
Source microkernel that has been formally proven to contain no runtime errors at the
source code level. “
We proved full functional correctness (which is a superset of absence of
runtime errors) for seL4 in 2009. I must be missing something.
Gernot
On 11 Mar 2016, at 6:50 , Jakub Jermář<[email protected]> wrote:
Hello,
just FYI, I have set up a simple web page[1] to promote the wider
microkernel community and its goals. So far, the page comes with a brief
description of the microkernel concept and an incomplete list of
microkernel projects with links to each project's web. The description
is made out of the first two sentences I found in the "What is XYZ"
section or elsewhere on the web of the respective project. I also took
the freedom to use the respective project's logo (or what I believed was
the project's logo) for promoting it.
I hope you will find this small web a good idea. It was inspired by a
similar (though a little bit more informative) site set up by the
unikernel community [2]. The sources of the [1] web are hosted on Github
[3], so feel free to submit issues or PR to make the site better.
Please send me a PM if there are any issues pertaining your project's
cartouche that cannot be dealt with using Github.
Thanks,
Jakub
[1] http://microkernel.info
[2] http://unikernel.org/projects/
[3] https://github.com/jermar/microkernel.info
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
