Couverture ElectroniqueS n°127

La jeune société belge Open License Society a fait appel à une méthode de modélisation formelle pour développer l'OS temps réel OpenComRTOS. Objectif : garantir l'absence d'erreurs dans le code et permettre à son utilisateur de vérifier n'importe quel aspect du logiciel. Pour Eric Verhulst, le fondateur de la jeune firme belge Open License Society, le marché des systèmes d'exploitation temps réel commerciaux vit une situation paradoxale. « A la base de nombreuses applications embarquées devant répondre à des contraintes strictes de sécurité et de sûreté de fonctionnement, la grande majorité de ces OS – à l'exception de portages spécifiques – ne peuvent pas être certifiés, et encore moins être vérifiés, explique M. Verhulst. La plupart du temps, c'est parce qu'il n'existe aucun document explicitant le processus de conception de l'OS. Le fait que certains OS temps réel soient disponibles avec le code source ne change rien à l'affaire, car, en général, les commentaires associés sont très succincts. Quant aux logiciels Open Source, ils sont rarement accompagnés d'un manuel utilisateur. » C'est ce constat qui a poussé Open License Society, créée en 2004, à se lancer début 2005 dans le développement d'un OS temps réel « vérifiable ». Dix-huit mois plus tard, le résultat est là. Elaboré selon une méthode de modélisation formelle qui garantit un code correct par construction, le système d'exploitation OpenComRTOS existe dans une version bêta et a déjà séduit le fabricant de capteurs Melexis (voir encadré).De manière générale, les méthodes formelles permettent, par le biais d'une modélisation mathématique, de raisonner rigoureusement sur des logiciels afin de démontrer leur validité par rapport à un ensemble de spécifications initiales. Une approche qui, selon Open License Society, est absolument nécessaire pour que les logiciels soient vérifiables, c'est-à-dire conformes aux spécifications.Inspiré de l'architecture de l'OS temps réel Virtuoso« Si le développeur d'une application critique ne peut pas réaliser lui-même cette vérification, il est obligé de faire confiance à l'éditeur de l'OS », note Eric Verhulst. C'est la raison pour laquelle l'éditeur belge accompagne OpenComRTOS d'un mode de commercialisation spécifique adapté et baptisé… « Open License ». Lors de l'achat, le développeur se verra ainsi remettre non seulement le code source mais également l'ensemble des documents nécessaires à la vérification de l'OS : descriptif des besoins, spécifications, modèles formels, exemples d'applications et jeux de tests.Au-delà de sa méthode de conception, OpenComRTOS se différencie aussi par son architecture, qui rappelle celle du noyau temps réel pour DSP Virtuoso commercialisé par Eonic Software avant son acquisition par Wind River en 2001. Société dont Eric Verhulst était le fondateur et le dirigeant. De fait, OpenComRTOS est doté d'une architecture multiniveau dont le niveau inférieur s'articule autour d'une couche de communication aisément extensible, peu gourmande en ressources et adaptée tant aux puces monoc&oelig;urs qu'aux circuits multic&oelig;urs, voire aux systèmes distribués hétérogènes. Référencé sous le nom de L0, ce niveau inférieur offre également les services basiques d'un noyau temps réel (démarrage et arrêt des tâches, ordonnancement préemptif, etc.). Ecrit pratiquement intégralement en langage C Ansi, il affiche une empreinte mémoire inférieure à 1 Ko pour une implantation monoprocesseur – un record mondial selon Eric Verhulst – et inférieure à 2 Ko dans une configuration multiprocesseur. « En fait, l'utilisation d'une méthode formelle lors de la conception de l'OS a aussi contribué au développement d'une architecture compacte, très “ propre ” et facilement portable », explique le dirigeant d'Open License Society.L'éditeur d'OpenComRTOS travaille actuellement au développement d'un niveau supérieur, dit L1, qui fournira des services supplémentaires que l'on trouve dans les OS temps réel traditionnels comme le support d'événements, de sémaphores ou de files d'attente Fifo. Sa première version devrait émuler l'API du système d'exploitation Virtuoso.Premier client : MelexisTrès présent dans le secteur automobile, Melexis a développé sous le nom de MelexCM une gamme de processeurs à double c&oelig;ur intégrant jusqu'à 32 Ko de mémoire flash programme et 2 Ko de mémoire données.Un programme test basé sur OpenComRTOS a été développé et porté sur un processeur MelexCM de 7,5 Mips. Le programme était constitué de deux tâches émettant et réceptionnant en continu des paquets de 8 octets pour une capacité de traitement globale de 9 574 paquets par seconde.L'espace mémoire requis s'est limité à 1 230 octets de mémoire flash et 228 octets de données. Le temps de réponse à une interruption a été mesuré à 55 µs.

L’OS temps réel devient « vérifiable » par son utilisateur

Couverture ElectroniqueS n°127

IBM grave les premières puces en 2 nm en abandonnant les FinFET

Zeta, le protocole LPWAN made in China, arrive en Europe

Harting invente le connecteur électronique sur mesure

L’OS temps réel devient « vérifiable » par son utilisateur

Dans la même rubrique

Couverture ElectroniqueS n°127

IBM grave les premières puces en 2 nm en abandonnant les FinFET

Zeta, le protocole LPWAN made in China, arrive en Europe

Harting invente le connecteur électronique sur mesure