Academic
Publications
Verification of behavioural elements of UML models using B

Verification of behavioural elements of UML models using B,10.1145/1066677.1067024,Ninh-Thuan Truong,Jeanine Souquieres

Verification of behavioural elements of UML models using B   (Citations: 2)
BibTex | RIS | RefWorks Download
This paper describes the formal verification of behavioural elements of UML models using B abstract machines. We transform the UML metamodel of behavioural diagrams to B and automatically check proof obligations generated by using the B prover. The correctness of the properties of behavioural elements of UML models is ensured by the well-formedness rules in the UML semantics which are transformed to B as the invariants of abstract machines. We address collaboration diagrams, state-chart diagrams of UML models and study the Behavioural Elements package (Collaboration and State Machine) of the UML metamodel as well as well-formedness rules of these packages. We illustrate our approach by a case study.
Conference: ACM Symposium on Applied Computing - SAC , pp. 1546-1552, 2005
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: