@Article{SantosSantVija:2014:TrUMBe,
               author = "Santos, Luciana Brasil Rebelo dos and Santiago J{\'u}nior, 
                         Valdivino Alexandre de and Vijaykumar, Nandamudi Lankalapalli",
          affiliation = "{Instituto Nacional de Pesquisas Espaciais (INPE)} and {Instituto 
                         Nacional de Pesquisas Espaciais (INPE)} and {Instituto Nacional de 
                         Pesquisas Espaciais (INPE)}",
                title = "Transformation of UML behavioral diagrams to support software 
                         model checking",
              journal = "Electronic Proceedings in Theoretical Computer Science",
                 year = "2014",
               volume = "147",
                pages = "133--142",
                 note = "{Setores de Atividade: Pesquisa e desenvolvimento 
                         cient{\'{\i}}fico.}",
             keywords = "model checking, UML, verification and validation.",
             abstract = "Unified Modeling Language (UML) is currently accepted as the 
                         standard for modeling (objectoriented) 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.",
                  doi = "10.4204/EPTCS.147.10",
                  url = "http://dx.doi.org/10.4204/EPTCS.147.10",
                 issn = "2075-2180",
                label = "lattes: 5039690360728170 2 
                         BrasilRebelodosSantosAlexLank:2014:TrUMBe",
             language = "en",
           targetfile = "1404.0855v1.pdf",
        urlaccessdate = "02 maio 2024"
}