Abstract
In the last decade, Model Driven Engineering (MDE) has been used to improve the development of safety critical systems by providing early Validation and Verification (V&V) tools for Domain Specific Modeling Languages (DSML). Verification of behavioral models is mainly addressed by translating domain specific models to formal verification dedicated languages in order to use the sophisticated associated tools such as model-checkers. This approach has been successfully applied in many different contexts, but it has a major drawback: the user has to interact with the formal tools. In this paper, we present an illustrated approach that allows the designer to formally express the expected behavioral properties using a user oriented language — a temporal extension of OCL —, that is automatically translated into the formal language; and then to get feedback from the assessment of these properties using its domain language without having to deal with the formal verification language nor with the underlying translational semantics. This work is based on the metamodeling pattern for executable DSML that extends the DSML metamodel to integrate concerns related to execution and behavior.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Farail, P., Gaufillet, P., Canals, A., Camus, C.L., Sciamma, D., Michel, P., Crégut, X., Pantel, M.: The TOPCASED project: a toolkit in open source for critical aeronautic systems design. In: Embedded Real Time Software (ERTS), Toulouse, France (January 2006)
Crégut, X., Combemale, B., Pantel, M., Faudoux, R., Pavei, J.: Generative Technologies for Model Animation in the TopCased Platform. In: Kühne, T., Selic, B., Gervais, M.-P., Terrier, F. (eds.) ECMFA 2010. LNCS, vol. 6138, pp. 90–103. Springer, Heidelberg (2010)
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(14), 2741–2756 (2004)
Software & Systems Process Engineering Metamodel (SPEM) 2.0, Object Management Group, Inc. (October 2007)
Combemale, B., Crégut, X., Giacometti, J.-P., Michel, P., Pantel, M.: Introducing Simulation and Model Animation in the MDE topcased Toolkit. In: Proceedings of the 4th European Congress Embedded Real Time Software (ERTS), Toulouse, France (2008)
Combemale, B.: Simulation et vérification de modèle par métamodélisation exécutable, E. U. Européennes, ed. (June 2010)
Ziemann, P., Gogolla, M.: An Extension of OCL with Temporal Logic. In: Jürjens, J., Cengarle, M.-V., Fernandez, E., Rumpe, B., Sandner, R. (eds.) Critical Systems Development with UML – Proceedings of the UML 2002 Workshop, vol. TUM-I0208, pp. 53–62, Université Technique de Munich, Institut d’Informatique (September 2002)
Combemale, B., Crégut, X., Garoche, P.-L., Thirioux, X., Vernadat, F.: A property-driven approach to formal verification of process models. In: ICEIS, Selected Papers (2007)
Jouault, F., Kurtev, I.: Transforming Models with ATL. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 128–138. Springer, Heidelberg (2006)
Bendraou, R., Combemale, B., Crégut, X., Gervais, M.-P.: Definition of an executable spem 2.0. In: APSEC, pp. 390–397. IEEE Computer Society (2007)
Hegedus, A., Bergmann, G., Rath, I., Varro, D.: Back-annotation of simulation traces with change-driven model transformations. In: IEEE International Conference on Software Engineering and Formal Methods, vol. 0, pp. 145–155 (2010)
Shah, S.M.A., Anastasakis, K., Bordbar, B.: From UML to Alloy and back again. In: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation (MODEVVA 2009). ACM International Conference Proceeding Series (2009)
Barber, K.S., Graser, T., Holt, J.: Providing early feedback in the development cycle through automated application of model checking to software architectures. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, ASE 2001 (2001)
Pelliccione, P., Inverardi, P., Muccini, H.: Charmy: A framework for designing and verifying architectural specifications. IEEE Trans. Soft. Eng. 35(3), 325–346 (2009)
Goldsby, H.J., Cheng, B.H.C., Konrad, S., Kamdoum, S.: A Visualization Framework for the Modeling and Formal Analysis of High Assurance Systems. In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol. 4199, pp. 707–721. Springer, Heidelberg (2006)
Lilius, J., Paltor, I.: vuml: a tool for verifying uml models. In: 14th IEEE International Conference on Automated Software Engineering, pp. 255–258 (October 1999)
Yu, J., Manh, T., Han, J., Jin, Y., Han, Y., Wang, J.: Pattern Based Property Specification and Verification for Service Composition, pp. 156–168 (2006)
Dwyer, M., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7–15. ACM Press (1998)
Autili, M., Inverardi, P., Pelliccione, P.: Graphical scenarios for specifying temporal properties: an automated approach. Automated Software Engg. 14, 293–340 (2007)
Berthomieu, B., Bodeveix, J.-P., Filali, M., Farail, P., Gaufillet, P., Garavel, H., Lang, F.: FIACRE: an Intermediate Language for Model Verification in the topcased Environment. In: 4th European Congress Embedded Real Time Software (ERTS) (January 2008)
Ljungkrantz, O., Akesson, K., Fabian, M., Yuan, C.: A formal specification language for plc-based control logic. In: 2010 8th IEEE International Conference on Industrial Informatics (INDIN), pp. 1067–1072 (July 2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zalila, F., Crégut, X., Pantel, M. (2012). Leveraging Formal Verification Tools for DSML Users: A Process Modeling Case Study. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies. ISoLA 2012. Lecture Notes in Computer Science, vol 7610. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34032-1_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-34032-1_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34031-4
Online ISBN: 978-3-642-34032-1
eBook Packages: Computer ScienceComputer Science (R0)