TY - GEN
T1 - An overview of a method and its support tool for generating B specifications from UML notations
AU - Laleau, R.
AU - Mammar, A.
N1 - Publisher Copyright:
© 2000 IEEE.
PY - 2000/1/1
Y1 - 2000/1/1
N2 - This paper presents, through an example, an overview of our method which generates B specifications from an application described using UML notations. We are interested in data intensive applications. This allows us to automatically generate basic update operations from class diagrams. Then these operations are combined to elaborate more complex transactions described in UML by state and collaboration diagrams. The obtained B machines are directly usable in AtelierB and proofs can be performed allowing the consistency of the application to be checked. Finally the outlines of the prototype support tool are described.
AB - This paper presents, through an example, an overview of our method which generates B specifications from an application described using UML notations. We are interested in data intensive applications. This allows us to automatically generate basic update operations from class diagrams. Then these operations are combined to elaborate more complex transactions described in UML by state and collaboration diagrams. The obtained B machines are directly usable in AtelierB and proofs can be performed allowing the consistency of the application to be checked. Finally the outlines of the prototype support tool are described.
U2 - 10.1109/ASE.2000.873675
DO - 10.1109/ASE.2000.873675
M3 - Conference contribution
AN - SCOPUS:84960891660
T3 - Proceedings ASE 2000: 15th IEEE International Conference on Automated Software Engineering
SP - 269
EP - 272
BT - Proceedings ASE 2000
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 15th IEEE International Conference on Automated Software Engineering, ASE 2000
Y2 - 11 September 2000 through 15 September 2000
ER -