Welcome to the InfoSci Platform
Formal Verification of a Subset of UML Diagrams: An Approach Using Maude

Formal Verification of a Subset of UML Diagrams: An Approach Using Maude

Allaoua Chaoui, Okba Tibermacine, Amer R. Zerek
Copyright: © 2011 |Pages: 11
ISBN13: 9781615207893|ISBN10: 1615207899|EISBN13: 9781615207909
DOI: 10.4018/978-1-61520-789-3.ch002
Cite Chapter Cite Chapter

MLA

Chaoui, Allaoua, et al. "Formal Verification of a Subset of UML Diagrams: An Approach Using Maude." Handbook of Research on E-Services in the Public Sector: E-Government Strategies and Advancements, edited by Abid Thyab Al Ajeeli and Yousif A. Latif Al-Bastaki, IGI Global, 2011, pp. 14-24. https://doi.org/10.4018/978-1-61520-789-3.ch002

APA

Chaoui, A., Tibermacine, O., & Zerek, A. R. (2011). Formal Verification of a Subset of UML Diagrams: An Approach Using Maude. In A. Al Ajeeli & Y. Al-Bastaki (Eds.), Handbook of Research on E-Services in the Public Sector: E-Government Strategies and Advancements (pp. 14-24). IGI Global. https://doi.org/10.4018/978-1-61520-789-3.ch002

Chicago

Chaoui, Allaoua, Okba Tibermacine, and Amer R. Zerek. "Formal Verification of a Subset of UML Diagrams: An Approach Using Maude." In Handbook of Research on E-Services in the Public Sector: E-Government Strategies and Advancements, edited by Abid Thyab Al Ajeeli and Yousif A. Latif Al-Bastaki, 14-24. Hershey, PA: IGI Global, 2011. https://doi.org/10.4018/978-1-61520-789-3.ch002

Export Reference

Mendeley
Favorite

Abstract

We introduce an approach that deals with the verification of UML collaboration and sequence diagrams in respect to the objects internal behaviors which are commonly represented by state machine diagrams. The approach is based on the translation of theses diagrams to Maude specifications. In fact, Maude is a declarative programming language, an executable formal specification language, and also a formal verification system, which permit the achievement of the approach goals. We define in details the rules of translating UML diagrams elements into their corresponding Maude specifications. We present the algebraic structures that represent the OR-States and the AND-states in a state machine diagram, and the structure that represents the collaboration and the sequence diagrams. Also, we explain the mechanism of the execution and the verification of the translated specification, which is based on rewriting logics rules.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.