| [pok-devel] Propose verifying the POK |
[ Thread Index |
Date Index
| More lists.tuxfamily.org/pok-devel Archives
]
I am a research visitor of the ACADIE group of IRIT in Toulouse. We are planning a proposal about verification of a real-time embedded operating system for safety-critical systems.
After analyzing the state of art, we found that POK is opensource and compatible with ARINC653. POK also has a very small kernel. Thus, we want to do verification of POK.
As the L4.verified Project (http://www.ertos.nicta.com.au/research/l4.verified/), we maybe use theorem proving.
Whether is it possible? Could you give us some suggestions?
On the other hand, POK has some open requirement or design document?