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 <mattiabotta...@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.hu...@embedded-brains.de > <mailto:sebastian.hu...@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.hu...@embedded-brains.de > <mailto:sebastian.hu...@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@rtems.org > http://lists.rtems.org/mailman/listinfo/users -------------------------------------------------------------------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@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/ --------------------------------------------------------------------
_______________________________________________ users mailing list users@rtems.org http://lists.rtems.org/mailman/listinfo/users
