Industrie Mag - Le journal de l'industrie.

PragmaDev annonce la sortie de la version 2.0 de son traceur maintenant baptisé PragmaDev Tracer, résultat du projet Européen PRESTO, qui introduit la vérification de propriétés.

PragmaDev Tracer met en oeuvre des représentations graphiques standards pour :

• Spécifier le comportement d’un système,
• Exprimer les propriétés d’un système,
• Tracer l’exécution dynamique d’un système évènementiel.

L’outil permet alors de vérifier qu’une trace d’exécution est conforme à une spécification et que les propriétés du système sont bien vérifiées lors de l’exécution.

Afin de faciliter la génération des traces, en particulier à partir de code existant, PragmaDev propose un ensemble de macros C qui génère des traces via une socket ou via un fichier.

Technologiquement l’outil met en oeuvre les technologies :
 MSC
— Le Message Sequence Chart est un standard de l’Union Internationale des Télécommunications sous la référence Z.120.

 Sequence Diagram
— Le Sequence Diagram est un des diagrammes de la notation UML définie par l’OMG.

 PSC
— Le Property Sequence Chart est une notation qui complète le MSC en permettant de définir les liens de causalité entre les différents évènements pour exprimer une propriété.

Enfin, l’outil stocke nativement ses diagrammes au format XML et peut lire le format textuel MSC ou des traces au format OTF.

http://www.pragmadev.com