The TOPCASED project - a Toolkit in OPen source for Critical Applications and SystEms Design

The TOPCASED project aims at developing an open source CASE environment for critical applications and systems development. Its main benefits should be to perpetuate the methods and tools for software development, minimize ownership costs, ensure independence of development platform, integrate, as soon as possible, methodological changes and advances made in academic world, be able to adapt tools to the process instead of the opposite, take into account qualification constraints. In this purpose, TOPCASED relies on the Eclipse Modelling Project platform (EMF, GEF, GMF, OCL, UML2, ...) and on many available tools such as the AMMA tools (ATL, AMW, AM3), MDDi model bus, Kermeta executable models, ... and participate in the development of extensions or additional tools. One key point is that TOPCASED focuses on critical system development, which means that a strong emphasis is made on system validation and on traceability. This paper focuses on the proposed process to help in designing correct systems by relying on DSL and formal approaches. Meta-modelling principles are at the core of the TOPCASED framework. We will focus on the example of SimplePDL a subset of the SPEM process modelling DSL. TOPCASED currently includes its own tool to automatically generate graphical editors for specific languages based on their metamodel. The demonstration will go through all the design of the DSL from the graphical editor, to the model validation called through the model bus. The paper focus on the model validation process. Until now, the only complete industrial solutions that are available at the meta-model level only consider structural properties such as the ones that could be expressed in OCL. There are although some attempts on behavioural properties for DSL. This paper addresses a method to specify and then check temporal properties over models. The case study is SIMPLEPDL, a process metamodel. We propose a way to use a temporal extension of OCL, TOCL, to express properties. We specify a models transformation to Petri Nets and LTL formulae for both the process model and its associated temporal properties. We check these properties using a model checker and enrich the model with the analysis results. This work is a first step towards a generic framework to specify and effectively check temporal properties over arbitrary models.