Le français PragmaDev, éditeur d’outils de développement et de test à base de modèles pour applications embarquées, met à disposition des développeurs une version gratuite de son outil Tracer, ...qui vérifie qu’une trace d’exécution est bien conforme à une spécification et que les propriétés du système sont bien vérifiées lors de son exécution. L’outil met notamment en œuvre des vues graphiques pour spécifier le comportement d’un système, exprimer les propriétés de ce même système et tracer l’exécution dynamique d’un système évènementiel.

Afin de faciliter la gestion des traces, PragmaDev  délivre un ensemble de fonctions en C qui génèrent des traces via un socket ou un fichier. Cet outil s’appuie sur les technologies MSC (Message Sequence Chart), norme éditée par l’UIT (Union Internationale des Télécommunications), Sequence Diagram, une notation de l’UML définie par l’OMG (Object Management Group), et PSC (Property Sequence Chart), notation qui complète le MSC. Il bénéficie également des résultats des travaux récemment menés au sein du projet de recherche européen Presto (imProvements of industrial Real time Embedded SysTems development PrOcess) qui fait partie du programme Artemis.