Abstract
More and more, models, through Domain Specific Languages (DSL), tend to be the solution to define complex systems. Expressing properties specific to these metamodels, and checking them, appear as an urgent need. Until now, the only complete industrial solutions that are available 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)
Object Management Group, Inc.: Software Process Engineering Metamodel (SPEM) 2.0 Specification, Final Adopted Specification (2007)
Bendraou, R., Combemale, B., Crégut, X., Gervais, M.P.: Definition of an Executable SPEM2.0. In: 14th APSEC, Japan. IEEE Computer Society, Los Alamitos (2007)
Cousot, P.: Methods and logics for proving programs. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), 841–994 (1990)
Object Management Group, Inc.: UML Object Constraint Language (OCL) 2.0 Specification, Final Adopted Specification (2003)
Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley Longman Publishing Co., Inc, Amsterdam (2003)
Richters, M., Gogolla, M.: Validating UML models and OCL constraints. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol. 1939, pp. 265–277. Springer, Heidelberg (2000)
Combemale, B., Rougemaille, S., Crégut, X., Migeon, F., Pantel, M., Maurel, C., Coulette, B.: Towards a rigorous metamodeling. In: 2nd International Workshop on Model-Driven Enterprise Information Systems, INSTICC (2006)
Combemale, B., Crégut, X., Berthomieu, B., Vernadat, F.: SimplePDL2Tina: Mise en oeuvre d’une Validation de Modede Processus. In: 3ieme journées sur l’Ingénierie Dirigée par les Modéles (IDM), Toulouse, France (2007)
Ziemann, P., Gogolla, M.: An extension of OCL with temporal logic. In: Critical Systems Development with UML – Proceedings of the UML 2002 workshop, vol. TUM-I0208, pp. 53–62 (2002)
Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA – construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research 42, 2741–2756 (2004)
Richters, M., Gogolla, M.: A metamodel for OCL. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 156–171. Springer, Heidelberg (1999)
Object Management Group, Inc.: Meta Object Facility (MOF) 2.0 Core Specification, Final Adopted Specification (2006)
Berthomieu, B., Vernadat, F.: Réseaux de Petri temporels : méthodes d’analyse et vérification avec TINA. Traité IC2 (2006)
Jouault, F., Kurtev, I.: Transforming models with ATL. In: Proceedings of the Model Transformations in Practice Workshop at MoDELS, Montego Bay, Jamaica (2005)
Jouault, F.: Loosely Coupled Traceability for ATL. In: Proceedings of the European Conference on Model Driven Architecture (ECMDA) workshop on traceability (2005)
Chen, K., Sztipanovits, J., Abdelwalhed, S., Jackson, E.: Semantic anchoring with model transformations. In: Hartman, A., Kreische, D. (eds.) ECMDA-FA 2005. LNCS, vol. 3748, pp. 115–129. Springer, Heidelberg (2005)
Gurevich, Y.: The abstract state machine paradigm: What is in and what is out. In: Ershov Memorial Conference (2001)
Agrawal, A., Karsai, G., Kalmar, Z., Neema, S., Shi, F., Vizhanyo, A.: The design of a language for model transformations. Technical report, Institute for Software Integrated Systems, Vanderbilt University, Nashville, USA (2005)
Clark, T., Evans, A., Sammut, P., Willans, J.: Applied metamodelling - a foundation for language driven development. version 0.1 (2004)
Flake, S.: Temporal OCL extensions for specification of real-time constraints. In: SVERTS at UML 2003, San Francisco, CA, USA (2003)
Flake, S., Mueller, W.: Formal semantics of static and temporal state-oriented OCL constraints. Journal on Software and System Modeling (SoSyM) 2 (2003)
Cengarle, M.V., Knapp, A.: Towards OCL/RT. In: International Symposium of Formal Methods Europe (FME) - Getting IT Right, pp. 390–409. Springer, London (2002)
Distefano, D., Katoen, J.P., Rensink, A.: Towards model checking OCL. In: ECOOP Workshop on Dening a Precise Semantics for UML (2000)
Bradfield, J.C., Filipe, J.K., Stevens, P.: Enriching OCL using observational mu-calculus. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 203–217. Springer, Heidelberg (2002)
Muller, P.A., Fleurey, F., Fondement, F., Hassenforder, M., Schneckenburger, R., Gérard, S., Jézéquel, J.M.: Model-driven analysis and synthesis of concrete syntax. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol. 4199. Springer, Heidelberg (2006)
Jouault, F., Bézivin, J., Kurtev, I.: TCS: a DSL for the Specification of Textual Concrete Syntaxes in Model Engineering. In: GPCE (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Combemale, B., Crégut, X., Garoche, PL., Thirioux, X., Vernadat, F. (2008). A Property-Driven Approach to Formal Verification of Process Models. In: Filipe, J., Cordeiro, J., Cardoso, J. (eds) Enterprise Information Systems. ICEIS 2007. Lecture Notes in Business Information Processing, vol 12. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88710-2_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-88710-2_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88709-6
Online ISBN: 978-3-540-88710-2
eBook Packages: Computer ScienceComputer Science (R0)