En poursuivant votre navigation sur ce site, vous acceptez l'utilisation de cookies pour vous proposer des contenus et services adaptés à vos centres d'intérêts. En savoir plus et gérer ces paramètres. OK X
 
 

 

 

Nouveaux produits

La nouvelle version gratuite du PragmaDev

Publication: Juin 2013

Partagez sur
 
L’outil permet alors de vérifier qu’une trace d’exécution est conforme à une spécification ...
 

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

Suivez Industrie Mag sur le Web

 

Newsletter

Inscrivez-vous a la newsletter d'Industrie Mag pour recevoir, régulièrement, des nouvelles du site par courrier électronique.

Email: