xSPEM, an eXecutable SPEM 2.0

News

• May 2008: the page dedicated to xSPEM is available !

General Overview

This page presents xSPEM, an eXecutable SPEM 2.0 metamodel, and tools for editing, simulating and verifying xSPEM process models. This work is an application of our work about model simulation and verification and follows a rigorous approach which is presented in the Benoit Combemale's PhD thesis. This thesis presents an approach for dynamic metamodeling (i.e. definition of DSML with behavioral semantics) in order to simulate and validate models. We also define generic tools for models simulation and properties formalization. In the last section we present other applications like simulation of UML2.0 state machines and formal verification of Ladder programs.

xSPEM Metamodel Description

The xSPEM metamodel is composed of four packages : three specific to the domain of process engineering (DDMM, SDMM and EDMM), and one general dedicated to the trace management (TM3). The metamodel follows the architecture described in the Figure 1.

Figure 1. Architecture for an Executable Metamodel

The xSPEM metamodel is presented in the Figure 2 and available as an Ecore file (and DI).

• The Domain Definition MetaModel (DDMM) is composed of two packages: the xSPEM_Core and the xSPEM_ProjectCharacteristics. The first one introduces the main concepts from SPEM 2.0 to define a structural process. The second one extend the first one by the project specific informations.
• The States Definition MetaModel (SDMM) is described by the xSPEM_ProcessObservability package. This package allows to caracterize all the possible states during an xSPEM process enactment.
• The Events Definition MetaModel (EDMM) is described by the xSPEM_EventDecriptions package which introduces the different events which allow to evolve the process execution.
• The Trace Management MetaModel (TM3) is a generic metamodel which helps to describe a sequence of events as a scenario or catch an execution through a trace.

Figure 2. The xSPEM Metamodel

Prototypes for process modeling and V&V

References

• Definition of an eXecutable SPEM2.0 [preprint.pdf] [.slide.pdf]
  R. Bendraou, B. Combemale, X. Crégut and M.-P. Gervais
  Accepted at APSEC'07, IEEE Computer Society, p. 390-397, December 05-07, 2007 - Nagoya, Japan
• Towards a Formal Verification of Process Model's Properties - SimplePDL and TOCL Case Study [.pdf] [.slide.pdf]
  B. Combemale, P.-L. Garoche, X. Crégut, X. Thirioux and F. Vernadat
  Accepted at ICEIS'07 (long paper), INSTICC, p. 80-89, June 12-16, 2007 - Funchal, Madeira - Portugal
• SimplePDL2Tina: Mise en oeuvre d'une Validation de Modèles de Processus [.pdf] [.slide.pdf]
  B. Combemale, X. Crégut, B. Berthomieu and F. Vernadat
  Accepted at IDM'07, March 29-30, 2007 - Toulouse, France
• TopProcess: A Process Model Driven Approach Applied in Topcased for Embedded Real-Time Software [.pdf]
  A. Garcia, B. Combemale, X. Crégut, J.-N. Guyot and B. Libert
  Accepted at ERTS'08, January 29-31, 2008 - Toulouse, France

Related Applications

Simulation of UML2.0 State Machines

A prototype of the UML2 StateMachines simulator has been developed following our generic architecture. It reuses the visualization of the model created while building the model with the Topcased graphical editor (DDMM). During simulation, it is possible to inspect the dynamic information of the model (SDMM) thanks to the dynamic simulation view. It is especially useful for the properties that are not graphically presented. A control view allows to control a simulation with a start button, a stop button and a step by step button. The simulation is either interactive or driven by a scenario chosen and loaded when the simulator is started. A batch mode is also possible.

• Download:
  The source code of the UML2.0 State Machine simulator are available on the CVS tree of the Topcased development server. It will be integrated in the next Topcased release (v2) synchronised with Eclipse Ganymede in July 2008.
• Publication:
  Introducing Simulation and Model Animation in the MDE Topcased Toolkit [.pdf]
  B. Combemale, X. Crégut, J.-P. Giacometti, P. Michel and M. Pantel
  Accepted at ERTS'08, January 29-31, 2008 - Toulouse, France

Formal Verification of Ladder Programs:

Ladder Diagram (LD) is the most used programming language for Programmable Logical Controllers (PLCs). A PLC is a special purpose industrial computer used to automate industrial processes. Bugs in LD programs are very costly and sometimes are even a threat to human safety.
We propose a model driven approach for formal verification of LD programs through model-checking. We provide a metamodel for a subset of the LD language. We define a time Petri net (TPN) semantics for LD programs through an ATL model transformation. Finally, we automatically generate behavioral properties over the LD models as LTL formulae which are then checked over the generated TPN using the model-checkers available in the Tina toolkit. We mainly focus on race condition detection.

• Download:
  A bundle is not currently available but will be released soon. You can checkout the source code from the subversion tree.
• Publication:
  Ladder Metamodeling & PLC Program Validation through Time Petri Nets
  D. Bender, B. Combemale, X. Crégut, J.-M. Farines, B. Berthomieu and F. Vernadat
  Accepted at ECMDA'08, June 09-12, 2008 - Berlin, Germany

Contact

IRIT laboratory, ACADIE team.

Site ENSEEIHT de l'IRIT-UMR CNRS 5505
Bâtiment I, Bureau I304
2, rue Charles Camichel - BP 7122
F-31071 TOULOUSE CEDEX 7

By email : benoit.combemale@(NO_SPAM)enseeiht.fr