A Formal Semantics for Use Case Diagram Via Event-B
2Institute of Mathematics and Statistics, University of São Paulo, São Paulo, 05508-090, Brazil.
Abstract—UML has become the "de facto" standard for modeling object-oriented software. However, the UML notation suffers from an imprecise and incomplete semantics definition, which makes difficult to automated analysis and is errors-prone. Formal methods have been used largely in order to deal with this problem. This paper proposes an approach to formally describe Use Case Diagram using the Event-B language. More specifically, it is presented a set of transformation rules that maps the elements of this diagram to elements of Event-B, both expressed via meta-models. The approach is illustrated by showing an example about how to make automatic verification in this diagram.
Index Terms—Formal semantics, use case diagram, event-B, formal verification.
Cite: Thiago C. de Sousa, Luciano Kelvin, Constantino Dias Neto, Carlos Giovanni N. de Carvalho, "A Formal Semantics for Use Case Diagram Via Event-B," Journal of Software vol. 12, no. 3, pp. 189-200, 2017.
May 03, 2016 News!
Papers published in JSW Vol. 11, No. 1- Vol. 11, No. 12 have been indexed by DBLP. [Click]
Jan 05, 2017 News!
[CFP] 2017 the annual meeting of JSW Editorial Board, ICCSM 2017, will be held in Maldives, July 4-6, 2017. [Click]
Apr 05, 2017 News!
Vol 12, No. 3 has been published with online version 7 original aritcles from 4 countries are published in this issue. [Click]
Sep 21, 2016 News!
Vol.11, No.8 has been indexed by EI (Inspec). [Click]
Nov 17, 2015 News!
Welcome Prof. Karim El Guemhioui from Canada to join the Editorial board of JSW. [Click]