On 6/3/07, Shams <shams@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 licensed,
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.

Thanks
Shams

_______________________________________________
l4-hackers mailing list
l4-hackers@os.inf.tu-dresden.de
http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers