|
Title:
|
VERIFICATION OF UML BEHAVIORAL DIAGRAMS USING SYMBOLIC MODEL CHECKING |
|
Author(s):
|
Flávio Fernandes, Mark Song |
|
ISBN:
|
978-989-8533-06-7 |
|
Editors:
|
Hans Weghorn, Leonardo Azevedo and Pedro Isaías |
|
Year:
|
2011 |
|
Edition:
|
Single |
|
Keywords:
|
Software Engineering, UML, Symbolic Model Checking, Symbolic Model Verifier |
|
Type:
|
Full Paper |
|
First Page:
|
11 |
|
Last Page:
|
18 |
|
Language:
|
English |
|
Cover:
|
|
|
Full Contents:
|
click to dowload 
|
|
Paper Abstract:
|
The Unified Modeling Language (UML) is a visual modeling language for specifying, visualizing, constructing and documenting artifacts of a system. Despite having many features to model systems UML lacks a formal semantic, which is essential to conduct verifications and validations. In this paper, the problem of performing verification of UML models is discussed through a proposed translation of UML behavioral diagrams to Symbolic Model Verifier (SMV) preserving the original semantic, thus making it possible to use Computation Tree Logic (CTL) to verify UML models. |
|
|
|
|
|
|
