Paper Info
Title
Towards A Wide Acceptance Of Formal Methods To The Design Of Safety Critical Software: An Approach Based On Uml And Model Checking
Abstract
The Unified Modeling Language (UML) is widely used to model systems for object oriented and/or embedded software development, specially by means of its several behavioral diagrams which can provide different points of view of the same software scenario. Model Checking is a formal verification method which has been receiving much attention from the academic community. However, in general, practitioners still avoid using Model Checking in their projects due to several reasons. Based on these facts, we present in this paper a significant improvement of a tool that we have developed which aims to translate several UML behavioral diagrams (sequence, activity, and state machine) into Transition Systems to support software Model Checking. With all the changes, we have applied our tool to a real space software product which is under development for a stratospheric balloon project to show how feasible is our approach in practice.
Year
DOI
Venue
2015
10.1007/978-3-319-21410-8_47
COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2015, PT IV
Keywords
Field
DocType
UML, Model Checking, XMITS, Behavioral diagrams
Model checking,Software engineering,UML tool,Unified Modeling Language,Computer science,Computer network,Applications of UML,Formal methods,Software verification and validation,Database,Diagramming software,Formal verification
Conference
Volume
ISSN
Citations 
9158
0302-9743
1
PageRank 
References 
Authors
0.37
15
4
Name
Order
Citations
PageRank
Eduardo Rohde Eras120.74
Luciana Brasil Rebelo dos Santos221.41
Valdivino Alexandre de Santiago Junior381.79
Nandamudi Lankalapalli Vijaykumar44913.63