Met OpencomRTOS introduceert Open License Society (OLS) uit Leuven naar eigen zeggen het eerste formeel ontworpen realtime besturingssysteem. De gelaagde nanokernelarchitectuur minimaliseert het geheugengebruik en de latency. De C-software is beschikbaar onder een open licentie waarbij gebruikers alle informatie krijgen, inclusief de ontwerpdocumentatie. Eerste klant is het Ieperse fabless chipbedrijf Melexis, dat OpencomRTOS op zijn automotive sensorplatform MelexCM zet.
’Open License Society vindt het RTOS opnieuw uit‘, kopt het persbericht. ’Dit is inderdaad een boude claim‘, beaamt OLS-directeur Eric Verhulst, ’maar in figuurlijke zin correct. We hebben een rigoureus systeemengineeringtraject gevolgd, waarbij we formele modellering hebben gebruikt om vanaf nul tot de finale architectuur en functionaliteit te komen. Samen met de Universiteit van Gent hebben we een wiskundig ontwerp gemaakt in de TLA+-taal, dat we vervolgens met de TLC-modelchecker hebben geverifieerd.‘
Virtuoso
OpencomRTOS is ontworpen als een schaalbare communicatielaag met scheduling tussen de verschillende taken. Omdat zowel de communicatie als de taakplanning verloopt met prioriteiten, is het ook te gebruiken als (gedistribueerd) realtime besturingssysteem. Boven op het compacte fundament komen een tussenniveau met traditionele RTOS-services en een toplaag die netwerkondersteuning biedt. Verder is het de bedoeling dat gebruikers hun eigen diensten kunnen toevoegen.
De eerste release is de zogeheten L0-laag. ’Die heeft alles om te mogen spreken van een hard realtime besturingssysteem: communicatie, geheugenbeheer, geprioriteerde taakplanning, synchronisatie. Het is een echte nanokernelarchitectuur, waarbij zelfs de kern en de drivers taken zijn met hun eigen prioriteit. Ook kun je meerdere OpencomRTOS-instanties op dezelfde processor plaatsen.‘
De twee bovenliggende lagen L1 en L2 verschijnen in de eerste respectievelijke de tweede helft van 2007, verwacht Verhulst. ’L1 biedt klassieke RTOS-objecten als events, Fifo‘s, mailboxen, pipe channels, resources en semaforen. Ook is er ondersteuning voor overerving van prioriteiten. In L0 hebben we die achterwege gelaten omwille van de eenvoud en het mindere belang voor kleine targetprocessoren. De L2-laag maakt meer dynamisch gedrag mogelijk. Verder werken we aan grafische ontwerpgereedschappen en richten we ons op support voor beveiliging en foutbestendigheid.‘
Voor de ontwikkeling hebben de Leuvenaren inspiratie opgedaan bij enkele Esa-projecten. Daarnaast konden ze profiteren van hun ervaring met het Virtuoso-RTOS, ontwikkeld door het Eonic Systems van Verhulst, later overgenomen door Wind River en inmiddels uit circulatie genomen. ’L1 komt grotendeels overeen met de Virtuoso-API. In zekere zin is OpencomRTOS de logische opvolger van dat RTOS. Voor een nieuwe versie hadden we sowieso van nul moeten herbeginnen, omdat de laatste editie van Virtuoso een eindegeneratieontwerp was.‘
Cleaner
Verhulst erkent dat de formele ontwikkeling van OpencomRTOS een hele uitdaging was. ’Toen we aan het project begonnen, was het niet evident dat we met gebruik van formele technieken een beter realtime besturingssysteem zouden bekomen. Het ontwerpen van een RTOS wordt een beetje beschouwd als een zwarte kunst en de literatuur over een formele aanpak gaat niet verder dan de scheduling.‘
Toch is niet alles goud wat er blinkt. ’Een verrassend resultaat van het project is dat formele technieken nog niet kunnen bewijzen dat een implementatie juist is. Je kunt alleen aantonen dat het model correct is. De kracht van formele modellering zit ‘m vooral in de ontwerpfase, omdat je dan tot een veel ’cleanere‘ oplossing komt. Natuurlijk kun je door reverse engineering een formeel model maken van een bestaand systeem, maar dat is minder productief dan de aanpak van in het begin toe te passen.‘
Voordeel van een formele benadering is dat deze een grotere zekerheid geeft in de correcte werking, zowel van de softwaremotor als van het gehele systeem. ’Doordat we OpencomRTOS zo hebben ontwikkeld, kunnen we spreken van een ’trustworthy component‘. Een toepassing die daarop is gebaseerd, zal sowieso betrouwbaarder zijn, onder meer omdat het gedrag van het realtime besturingssysteem heel nauwkeurig gekend is. Het formele RTOS-model is te gebruiken in het formele model van de applicaties. Dat belet niet dat we nog een validatiefase moeten doorlopen om volledig zeker te zijn, maar dat geldt voor elk systeemontwerp.‘
Toets aan de werkelijkheid
Open License Society richt zich met OpencomRTOS op diep ingebedde systemen met DSP‘s, FPGA‘s, multicore-CPU‘s of processoren met zeer weinig geheugen. Daarbij denkt Verhulst aan beveiligingstoepassingen en sensornetwerken. ’Maar het applicatiedomein is heel breed. De communicatielaag op zichzelf kan ook dienen om heterogene systemen op een eenvoudige manier aan elkaar te knopen.‘
Melexis is de eerste klant. De IC-leverancier aan de automotive- en consumentenmarkt gaat OpencomRTOS gebruiken met zijn nieuwe MelexCM-chip, een 7,5 Mips ASSP-bouwsteen met 2 kbyte data-Ram en 32 kbyte flash. ’Die wordt daarmee een van de eerste slimme sensoren met een echt realtime besturingssysteem‘, aldus Verhulst.
Vorig jaar startte Open License Society een nieuwe businessunit voor software- en systeemdiensten bij de Ieperaren. ’Melexis is een sponsorend lid van OLS en wij bieden onze diensten aan op niet-exclusieve basis. De samenwerking is een partnerschap, waarbij wij onze kennis bij hen in de praktijk brengen. Dat geeft ons een prima toets van echte ontwerpen aan de werkelijkheid, vooral in automotive.‘