文献类型： 会议论文

第一作者： Angel Garcia

作者： Angel Garcia ¹ ; Benoit Combemale ² ; Xavier Cregut ² ; Jean-Nol Guyot ² ; Boris Libert ² ;

作者机构： 1.Tectosages, Parc Technologique Delta Sud Cap Delta

2.IRIT - University of Toulouse

会议名称： European Congress on Embedded Real Time Software

主办单位：

页码： 429-438

摘要： In this paper we present the work undertaken in the context of the TOPCASED R&D project (Toolkit in OPen source for Critical Applications & SystEms Development), which aims at providing an open source toolkit for the development of critical applications (embedded, real-time) and systems. The TOPCASED project defines quality requirements that must be ensured in the process used for the construction of its tools. The contribution of this paper consists in a method that 1) verify that a process respects these quality requirements and 2) verify the termination property of the process according to expressed constraints (scheduling, resource, time). Respect of quality requirements is achieved by explicitly modelling what parts of the process cover which requirements. Models are based on OMG SPEM2.0 metamodel and may be defined using the Eclipse Process Framework (EPF). To achieve verification of process models, we translate process models into equivalent Petri net models, and properties on the process into LTL (Linear Temporal Logic) formulae on the Petri net model. We then use the Tina toolkit (TIme petri Net Analyzer) and in particular its model-checker to check whether the properties hold.

分类号： TP311.5-53