Abstract
Validation of a system design enables to discover specification errors before it is implemented (or tested), thus hopefully reducing the development cost and time. The Unified Modelling Language (UML) is becoming widely accepted for the early specification and analysis of requirements for safety-critical systems, although a better balance between UML’s undisputed flexibility, and a precise unambiguous semantics, is needed. In this paper we introduce UMerL, a tool that is capable of executing and formally verifying UML diagrams (namely, UML state machine, class and object diagrams) by means of a translation of its behavioural information into Erlang. The use of the tool is illustrated with an example in embedded software design.
The research has received funding from the ARTEMIS JU: grant agreement 295373 (nSafeCer), from the Spanish MINECO: STRONGSOFT (TIN2012-39391-C04-02), and from the Comunidad Autónoma de Madrid: PROMETIDOS (P2009/TIC-1465).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent Programming in Erlang. Prentice-Hall (1996)
Liu, S., Liu, Y., Sun, J., Zheng, M., Wadhwa, B., Dong, J.S.: USMMC: A Self-contained Model Checker for UML State Machines. In: Proc. of the 2013 Meeting on Foundations of Software Engineering, pp. 623–626. ACM, New York (2013)
Lilius, J., Paltor, I.P.: Formalising UML State Machines for Model Checking. In: France, R., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 430–444. Springer, Heidelberg (1999)
Balser, M., Bäumler, S., Knapp, A., Reif, W., Thums, A.: Interactive verification of UML state machines. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 434–448. Springer, Heidelberg (2004)
Arts, T., Hughes, J., Johansson, J., Wiger, U.: Testing Telecoms Software with Quviq QuickCheck. In: ACM SIGPLAN Int. Erlang Workshop. ACM (2006)
Fredlund, L.Å., Svensson, H.: McErlang: a model checker for a distributed functional programming language. In: 12th ACM SIGPLAN ICFP. ACM (2007)
Pnueli, A.: The Temporal Logic of Programs. In: FOCS, pp. 46–57 (1977)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Rodríguez, R.J., Fredlund, LÅ., Herranz, Á., Mariño, J. (2014). Execution and Verification of UML State Machines with Erlang. In: Giannakopoulou, D., Salaün, G. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science, vol 8702. Springer, Cham. https://doi.org/10.1007/978-3-319-10431-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-10431-7_22
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10430-0
Online ISBN: 978-3-319-10431-7
eBook Packages: Computer ScienceComputer Science (R0)