Delay until in Ada seems not to work

[Andrew Butterfield]

Hi Mattia,
  this is very interesting.

Previous work I did for ESA using formal methods was looking at separation kernel verification,
with XtratuM code as an example. I remember that common use case was where one 
of the seperation kernel partitions contained an instance of RTEMS - I understand a demonstration system was
built. Now I am looking at verification of key managers within RTEMS-SMP.

Regards,
  Andrew Butterfield

> On 27 Jan 2021, at 14:27, Mattia Bottaro <mattiabottaro9 at gmail.com> wrote:
> 
> I've not specified it because I'm in a "non-conventional" situation: I'm running RTEMS over XtratuM: <https://fentiss.com/products/hypervisor/ <https://fentiss.com/products/hypervisor/>>.
> I'm using a BSP developed by FentISS. The hardware is the zynq7000.
> 
> Il giorno mer 27 gen 2021 alle ore 14:25 Sebastian Huber <sebastian.huber at embedded-brains.de <mailto:sebastian.huber at embedded-brains.de>> ha scritto:
> On 27/01/2021 11:54, Mattia Bottaro wrote:
> 
> > If you look at rtems_init.c file in that folder 
> > (<https://git.rtems.org/ada-examples/snapshot/ada-examples-4-10-2.tar.bz2 <https://git.rtems.org/ada-examples/snapshot/ada-examples-4-10-2.tar.bz2> 
> > <https://git.rtems.org/ada-examples/snapshot/ada-examples-4-10-2.tar.bz2 <https://git.rtems.org/ada-examples/snapshot/ada-examples-4-10-2.tar.bz2>>>), 
> > you can see that there is no time of day. I thought it was ok since 
> > I'm running an example.
> >
> > Anyway, I've added time of day in rtems_init.c with these values: 
> > https://github.com/RTEMS/rtems-examples/blob/master/classic_api/triple_period/init.c#L39 <https://github.com/RTEMS/rtems-examples/blob/master/classic_api/triple_period/init.c#L39> 
> > <https://github.com/RTEMS/rtems-examples/blob/master/classic_api/triple_period/init.c#L39 <https://github.com/RTEMS/rtems-examples/blob/master/classic_api/triple_period/init.c#L39>>. 
> >
> > I've also set it with status = rtems_clock_set( &time) , but the 
> > behaviour does not change.
> On which BSP and hardware did you try this out?
> 
> -- 
> embedded brains GmbH
> Herr Sebastian HUBER
> Dornierstr. 4
> 82178 Puchheim
> Germany
> email: sebastian.huber at embedded-brains.de <mailto:sebastian.huber at embedded-brains.de>
> phone: +49-89-18 94 741 - 16
> fax:   +49-89-18 94 741 - 08
> 
> Registergericht: Amtsgericht München
> Registernummer: HRB 157899
> Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
> Unsere Datenschutzerklärung finden Sie hier:
> https://embedded-brains.de/datenschutzerklaerung/ <https://embedded-brains.de/datenschutzerklaerung/>
> 
> _______________________________________________
> users mailing list
> users at rtems.org
> http://lists.rtems.org/mailman/listinfo/users

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero at TCD, Head of Software Foundations & Verification Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.rtems.org/pipermail/users/attachments/20210127/268385d4/attachment-0001.html>