New free version of PragmaDev Tracer can verify properties.

Date 2013/6/5 9:59:00 | Topic: Product News

PragmaDev, the leading SDL modeling tool vendor, introduces the result of PRESTO European project: PragmaDev Tracer V2.0. This brand new version has been fully redesigned and is capable of verifying properties on execution traces.
PragmaDev Tracer implements standard graphical representations to:
* Specify the behavior of a system,
* Define the properties of a system,
* Trace the execution of an event driven system.

The tool can verify an execution trace conforms to a specification and to the properties.

To ease trace generation, especially from legacy code, PragmaDev provides a set of C macros to generate traces through a socket or in a file.
PragmaDev Tracer implements a set of technologies:
* MSC: Message Sequence Chart is an ITU standard under reference Z.120.
* Sequence Diagram: Sequence Diagram is one of the UML diagrams defined by the OMG.
* PSC: Property Sequence Chart is a notation that completes the MSC in order to define causality between events in order to express a property.

The tool native storage format is XML and can read the MSC textual representation or OTF files.

About PragmaDev

PragmaDev is a privately held company based in Paris France that provides since 2001 a set of model driven tools dedicated to the development and test of real time and embedded software: Real Time DeveloperStudio. Customers include Airbus, Alcatel, Renault, the French Army, Wipro, Thomson, ST-Ericsson, Korean Telecom, ESA, Toshiba, and LG Electronics.

This article comes from Software Development Tools

The URL for this story is: