Abstract
The application of formal methods (especially, model checking and static analysis techniques) for the verification of safety critical embedded systems has produced very good results and raised the interest of system designers up to the application of these technologies in real size projects. However, these methods usually rely on specific verification oriented formal languages that most designers do not master. It is thus mandatory to embed the associated tools in automated verification toolchains that allow designers to rely on their usual domain-specific modeling languages (DSMLs) while enjoying the benefits of these powerful methods. More precisely, we propose a language to formally express system requirements and interpret verification results so that system designers (DSML end-users) avoid the burden of learning some formal verification technologies. Formal verification is achieved through translational semantics. This work is based on a metamodeling pattern for executable DSML that favors the definition of generative tools and thus eases the integration of tools for new DSMLs.
This works was funded by the french Ministry of Industry through the ITEA2 project OPEES and the french ANR project GEMOC.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Merilinna, J., Pärssinen, J.: Verification and validation in the context of domain-specific modelling. In: Proceedings of the 10th Workshop on Domain-Specific Modeling, ser. DSM 2010, pp. 9:1–9:6. ACM, New York (2010), http://doi.acm.org/10.1145/2060329.2060351
Harel, D., Rumpe, B.: Meaningful Modeling: What’s the Semantics of “Semantics”? Computer 37(10), 64–72 (2004)
Combemale, B., Crégut, X., Pantel, M.: A Design Pattern to Build Executable DSMLs and associated V&V tools (short paper). In: Asia-Pacific Software Engineering Conference (APSEC), Hong Kong, China (2012)
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 (September 2002)
Software & Systems Process Engineering Metamodel (SPEM) 2.0. Object Management Group, Inc. (October 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: ERTS 2008 (January 2008)
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 (January 2008)
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)
Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA – construction of abstract state spaces for Petri nets and time Petri nets. Int. Journal of Production Research 42(14), 2741–2756 (2004)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2010: A toolbox for the construction and analysis of distributed processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Correa, T., Becker, L., Farines, J.-M., Bodeveix, J.-P., Filali, M., Vernadat, F.: Supporting the Design of Safety Critical Systems Using AADL. In: 2010 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 331–336 (March 2010)
Farines, J.-M., De Queiroz, M.H., De Rocha, V., Carpes, A.M., Vernadat, F., Crégut, X.: A model-driven engineering approach to formal verification of PLC programs (regular paper). In: Emerging Technologies and Factory Automation (ETFA), Toulouse, France, pp. 1–8. IEEE (2011)
Jouault, F., Kurtev, I.: Transforming Models with ATL. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 128–138. Springer, Heidelberg (2006)
Eclipse, Acceleo (2012), http://www.eclipse.org/acceleo/
Abid, N., Dal-Zilio, S., Botlan, D.L.: A verified approach for checking real-time specification patterns. CoRR, vol. abs/1301.7531 (2013)
Zalila, F., Crégut, X., Pantel, M.: Verification results feedback for Fiacre intermediate language. In: Confrence en Ingnierie du Logiciel, CIEL (June 2012), http://gpl2012.irisa.fr/?q=node/31
Abid, N., Dal Zilio, S.: Real-time Extensions for the Fiacre modeling language (2010), http://automata.rwth--aachen.de/movep2010/index.php?page=about , http://hal.archives-ouvertes.fr/hal-00593958
Zalila, F., Crégut, X., Pantel, M.: Leveraging formal verification tools for DSML users: a process modeling case study. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 329–343. Springer, Heidelberg (2012), http://hal.archives-ouvertes.fr/hal-00720917
Jouault, F.: Loosely coupled traceability for ATLl. In: Proceedings of the European Conference on Model Driven Architecture (ECMDA) Workshop on Traceability (2005)
Chen, X., Hsieh, H., Balarin, F.: Verification approach of metropolis design framework for embedded systems. International Journal of Parallel Programming 34(1), 3–27 (2006)
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 ASE 2001, Washington, DC, USA (2001)
Hegedüs, Á., Bergmann, G., Ráth, I., Varró, D.: Back-annotation of simulation traces with change-driven model transformations. In: SEFM 2010, pp. 145–155 (2010)
Combemale, B., Gonnord, L., Rusu, V.: A generic tool for tracing executions back to a dSML’s operational semantics. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol. 6698, pp. 35–51. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zalila, F., Crégut, X., Pantel, M. (2013). Formal Verification Integration Approach for DSML. In: Moreira, A., Schätz, B., Gray, J., Vallecillo, A., Clarke, P. (eds) Model-Driven Engineering Languages and Systems. MODELS 2013. Lecture Notes in Computer Science, vol 8107. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41533-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-41533-3_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41532-6
Online ISBN: 978-3-642-41533-3
eBook Packages: Computer ScienceComputer Science (R0)