<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class="">Hi Mattia,<div class=""> this is very interesting.</div><div class=""><br class=""></div><div class="">Previous work I did for ESA using formal methods was looking at separation kernel verification,</div><div class="">with XtratuM code as an example. I remember that common use case was where one </div><div class="">of the seperation kernel partitions contained an instance of RTEMS - I understand a demonstration system was</div><div class="">built. Now I am looking at verification of key managers within RTEMS-SMP.</div><div class=""><br class=""></div><div class="">Regards,</div><div class=""> Andrew Butterfield</div><div class=""></div><div><br class=""><blockquote type="cite" class=""><div class="">On 27 Jan 2021, at 14:27, Mattia Bottaro <<a href="mailto:mattiabottaro9@gmail.com" class="">mattiabottaro9@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">I've not specified it because I'm in a "non-conventional" situation: I'm running RTEMS over XtratuM: <<a href="https://fentiss.com/products/hypervisor/" class="">https://fentiss.com/products/hypervisor/</a>>.<div class="">I'm using a BSP developed by FentISS. The hardware is the zynq7000.</div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Il giorno mer 27 gen 2021 alle ore 14:25 Sebastian Huber <<a href="mailto:sebastian.huber@embedded-brains.de" class="">sebastian.huber@embedded-brains.de</a>> ha scritto:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 27/01/2021 11:54, Mattia Bottaro wrote:<br class="">
<br class="">
> If you look at rtems_init.c file in that folder <br class="">
> (<<a href="https://git.rtems.org/ada-examples/snapshot/ada-examples-4-10-2.tar.bz2" rel="noreferrer" target="_blank" class="">https://git.rtems.org/ada-examples/snapshot/ada-examples-4-10-2.tar.bz2</a> <br class="">
> <<a href="https://git.rtems.org/ada-examples/snapshot/ada-examples-4-10-2.tar.bz2" rel="noreferrer" target="_blank" class="">https://git.rtems.org/ada-examples/snapshot/ada-examples-4-10-2.tar.bz2</a>>>), <br class="">
> you can see that there is no time of day. I thought it was ok since <br class="">
> I'm running an example.<br class="">
><br class="">
> Anyway, I've added time of day in rtems_init.c with these values: <br class="">
> <a href="https://github.com/RTEMS/rtems-examples/blob/master/classic_api/triple_period/init.c#L39" rel="noreferrer" target="_blank" class="">https://github.com/RTEMS/rtems-examples/blob/master/classic_api/triple_period/init.c#L39</a> <br class="">
> <<a href="https://github.com/RTEMS/rtems-examples/blob/master/classic_api/triple_period/init.c#L39" rel="noreferrer" target="_blank" class="">https://github.com/RTEMS/rtems-examples/blob/master/classic_api/triple_period/init.c#L39</a>>. <br class="">
><br class="">
> I've also set it with status = rtems_clock_set( &time) , but the <br class="">
> behaviour does not change.<br class="">
On which BSP and hardware did you try this out?<br class="">
<br class="">
-- <br class="">
embedded brains GmbH<br class="">
Herr Sebastian HUBER<br class="">
Dornierstr. 4<br class="">
82178 Puchheim<br class="">
Germany<br class="">
email: <a href="mailto:sebastian.huber@embedded-brains.de" target="_blank" class="">sebastian.huber@embedded-brains.de</a><br class="">
phone: +49-89-18 94 741 - 16<br class="">
fax: +49-89-18 94 741 - 08<br class="">
<br class="">
Registergericht: Amtsgericht München<br class="">
Registernummer: HRB 157899<br class="">
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler<br class="">
Unsere Datenschutzerklärung finden Sie hier:<br class="">
<a href="https://embedded-brains.de/datenschutzerklaerung/" rel="noreferrer" target="_blank" class="">https://embedded-brains.de/datenschutzerklaerung/</a><br class="">
<br class="">
</blockquote></div>
_______________________________________________<br class="">users mailing list<br class=""><a href="mailto:users@rtems.org" class="">users@rtems.org</a><br class="">http://lists.rtems.org/mailman/listinfo/users</div></blockquote></div><br class=""><div class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">--------------------------------------------------------------------<br class="">Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204<br class="">Lero@TCD, Head of Software Foundations & Verification Research Group<br class="">School of Computer Science and Statistics,<br class="">Room G.39, O'Reilly Institute, Trinity College, University of Dublin<br class=""> <a href="http://www.scss.tcd.ie/Andrew.Butterfield/" class="">http://www.scss.tcd.ie/Andrew.Butterfield/</a><br class="">--------------------------------------------------------------------</div>
</div>
<br class=""></body></html>