jorge.torres.maldonado at gmail.com
Sun Jun 3 11:30:43 CEST 2007
On 6/3/07, Shams <shams at orcon.net.nz> wrote:
> 1. Is OKL4 is a commercial implementation of L4?
I'm not sure about what you mean by commercial, but OKL4 is still BSD
As far as I understand, Open kernel labs is a son of NICTA, with the purpose
of commercializing ERTOS research program developments, you may find more
information about this at NICTA's web site.
2. Is OKL4 based on the L4.Pistachio code base and still open-source
> but with a separate source tree?
L4.Pistachio is developed and maintained by the System Architecture Group
at the University of Karlsruhe, people from U of new south wales used it to
make their l4.embedded, and added a minimal OS personality called iguana,
the L4.embedded API has changed a lot in the last year, and it is now
released under the name of OKL4, by open kernel labs.
OKL4=OKL4 microkernel + iguana + wombat
3. The OKL4 roadmap http://www.ok-labs.com/products/product_roadmap
> mentions "High-security API" and "Formal correctness proof".
What I understand is that the formal correctness proof its being worked in
team with NICTA, using Isabelle.
Does this mean that L4.Sec may or is already getting implemented in OKL4?
I think they are two different things.
Well hope it helps.
> l4-hackers mailing list
> l4-hackers at os.inf.tu-dresden.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the l4-hackers