Re: [pok-devel] Propose verifying the POK

[Jérôme Hugues <Jerome.HUGUES@xxxxxxx>]

Hi,

Le 6 févr. 2013 à 09:39, "Zhao YONGWANG" <Zhao.Yongwang@xxxxxxx> a écrit :

> 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?

There is a tricky aspect: L4 was verified for security, whereas you would want to verify POK for timing and safety
proving safety is in the scope of theorem proving I guess

For what concern timing, I'm not sure theorem proving would help. Perhaps timed automata or similar formalism would help

Also, POK has no validation test suite, simply to check that the behavior is the expected one. I guess one would need to allocate resources prior to do theorem proving: proving an incorrect design is hard, proving a program that seems to provide a correct output would make more sense

> On the other hand, POK has some open requirement or design document?


I remember Julien Delange and Laurent Lec did a paper presenting the architecture. 
Also, PhD manuscript by Julien has some details, but it is written in French

Regards,

--
Jérôme Hugues, ISAE/DMIA
Jerome.HUGUES@xxxxxxx - (+33) 5 61 33 91 84

BEGIN:VCARD
VERSION:3.0
N:Hugues;Jérôme;;;
FN:Hugues Jérôme
ORG:ISAE;
EMAIL;type=INTERNET;type=WORK;type=pref:Jerome.Hugues@xxxxxxx
TEL;type=WORK;type=pref:+33 5 61 33 91 84
item1.ADR;type=WORK;type=pref:;;10 avenue Edouard Belin - BP 54032;Toulouse CEDEX 4;;31055;France
item1.X-ABADR:fr
item2.X-ABRELATEDNAMES;type=pref:6
item2.X-ABLabel:_$!<Friend>!$_
X-ABUID:1C4FE2F0-51B7-4C40-85A1-B4E43A5FE1B5\:ABPerson
END:VCARD