Transformation of UML Behavioral Diagrams to Support Software Model Checking

Transformation of UML Behavioral Diagrams to Support Software Model Checking. Santos, L. B. R. d., Júnior, V. A. d. S., & Vijaykumar, N. L. In Electronic Proceedings in Theoretical Computer Science, volume 147, pages 133–142, April, 2014.

Paper doi abstract bibtex

Unified Modeling Language (UML) is currently accepted as the standard for modeling (object-oriented) software, and its use is increasing in the aerospace industry. Verification and Validation of complex software developed according to UML is not trivial due to complexity of the software itself, and the several different UML models/diagrams that can be used to model behavior and structure of the software. This paper presents an approach to transform up to three different UML behavioral diagrams (sequence, behavioral state machines, and activity) into a single Transition System to support Model Checking of software developed in accordance with UML. In our approach, properties are formalized based on use case descriptions. The transformation is done for the NuSMV model checker, but we see the possibility in using other model checkers, such as SPIN. The main contribution of our work is the transformation of a non-formal language (UML) to a formal language (language of the NuSMV model checker) towards a greater adoption in practice of formal methods in software development.

@inproceedings{santos_transformation_2014,
	title = {Transformation of {UML} {Behavioral} {Diagrams} to {Support} {Software} {Model} {Checking}},
	volume = {147},
	url = {http://arxiv.org/abs/1404.0855},
	doi = {10/ghv52v},
	abstract = {Unified Modeling Language (UML) is currently accepted as the standard for modeling (object-oriented) software, and its use is increasing in the aerospace industry. Verification and Validation of complex software developed according to UML is not trivial due to complexity of the software itself, and the several different UML models/diagrams that can be used to model behavior and structure of the software. This paper presents an approach to transform up to three different UML behavioral diagrams (sequence, behavioral state machines, and activity) into a single Transition System to support Model Checking of software developed in accordance with UML. In our approach, properties are formalized based on use case descriptions. The transformation is done for the NuSMV model checker, but we see the possibility in using other model checkers, such as SPIN. The main contribution of our work is the transformation of a non-formal language (UML) to a formal language (language of the NuSMV model checker) towards a greater adoption in practice of formal methods in software development.},
	urldate = {2021-01-27},
	booktitle = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},
	author = {Santos, Luciana Brasil Rebelo dos and Júnior, Valdivino Alexandre de Santiago and Vijaykumar, Nandamudi Lankalapalli},
	month = apr,
	year = {2014},
	keywords = {Computer Science - Software Engineering},
	pages = {133--142},
}

Downloads: 0

{"_id":"6n4EKLywtmNCQ5Mt9","bibbaseid":"santos-jnior-vijaykumar-transformationofumlbehavioraldiagramstosupportsoftwaremodelchecking-2014","author_short":["Santos, L. B. R. d.","Júnior, V. A. d. S.","Vijaykumar, N. L."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Transformation of UML Behavioral Diagrams to Support Software Model Checking","volume":"147","url":"http://arxiv.org/abs/1404.0855","doi":"10/ghv52v","abstract":"Unified Modeling Language (UML) is currently accepted as the standard for modeling (object-oriented) software, and its use is increasing in the aerospace industry. Verification and Validation of complex software developed according to UML is not trivial due to complexity of the software itself, and the several different UML models/diagrams that can be used to model behavior and structure of the software. This paper presents an approach to transform up to three different UML behavioral diagrams (sequence, behavioral state machines, and activity) into a single Transition System to support Model Checking of software developed in accordance with UML. In our approach, properties are formalized based on use case descriptions. The transformation is done for the NuSMV model checker, but we see the possibility in using other model checkers, such as SPIN. The main contribution of our work is the transformation of a non-formal language (UML) to a formal language (language of the NuSMV model checker) towards a greater adoption in practice of formal methods in software development.","urldate":"2021-01-27","booktitle":"Electronic Proceedings in Theoretical Computer Science","author":[{"propositions":[],"lastnames":["Santos"],"firstnames":["Luciana","Brasil","Rebelo","dos"],"suffixes":[]},{"propositions":[],"lastnames":["Júnior"],"firstnames":["Valdivino","Alexandre","de","Santiago"],"suffixes":[]},{"propositions":[],"lastnames":["Vijaykumar"],"firstnames":["Nandamudi","Lankalapalli"],"suffixes":[]}],"month":"April","year":"2014","keywords":"Computer Science - Software Engineering","pages":"133–142","bibtex":"@inproceedings{santos_transformation_2014,\n\ttitle = {Transformation of {UML} {Behavioral} {Diagrams} to {Support} {Software} {Model} {Checking}},\n\tvolume = {147},\n\turl = {http://arxiv.org/abs/1404.0855},\n\tdoi = {10/ghv52v},\n\tabstract = {Unified Modeling Language (UML) is currently accepted as the standard for modeling (object-oriented) software, and its use is increasing in the aerospace industry. Verification and Validation of complex software developed according to UML is not trivial due to complexity of the software itself, and the several different UML models/diagrams that can be used to model behavior and structure of the software. This paper presents an approach to transform up to three different UML behavioral diagrams (sequence, behavioral state machines, and activity) into a single Transition System to support Model Checking of software developed in accordance with UML. In our approach, properties are formalized based on use case descriptions. The transformation is done for the NuSMV model checker, but we see the possibility in using other model checkers, such as SPIN. The main contribution of our work is the transformation of a non-formal language (UML) to a formal language (language of the NuSMV model checker) towards a greater adoption in practice of formal methods in software development.},\n\turldate = {2021-01-27},\n\tbooktitle = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},\n\tauthor = {Santos, Luciana Brasil Rebelo dos and Júnior, Valdivino Alexandre de Santiago and Vijaykumar, Nandamudi Lankalapalli},\n\tmonth = apr,\n\tyear = {2014},\n\tkeywords = {Computer Science - Software Engineering},\n\tpages = {133--142},\n}\n\n","author_short":["Santos, L. B. R. d.","Júnior, V. A. d. S.","Vijaykumar, N. L."],"key":"santos_transformation_2014","id":"santos_transformation_2014","bibbaseid":"santos-jnior-vijaykumar-transformationofumlbehavioraldiagramstosupportsoftwaremodelchecking-2014","role":"author","urls":{"Paper":"http://arxiv.org/abs/1404.0855"},"keyword":["Computer Science - Software Engineering"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/SilverSylvester","dataSources":["YCBcQPneB9oxahSnp"],"keywords":["computer science - software engineering"],"search_terms":["transformation","uml","behavioral","diagrams","support","software","model","checking","santos","júnior","vijaykumar"],"title":"Transformation of UML Behavioral Diagrams to Support Software Model Checking","year":2014}