@InProceedings{SantosSantVija:2013:AlTrUM,
               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 = "An algorithm to translate UML behavioral diagrams for formal 
                         verification",
            booktitle = "Anais...",
                 year = "2013",
         organization = "Workshop dos Cursos de Computa{\c{c}}{\~a}o Aplicada do INPE, 
                         13. (WORCAP)",
            publisher = "INPE",
              address = "S{\~a}o Jos{\'e} dos Campos",
             keywords = "Model Checking, UML, Verifica{\c{c}}{\~a}o Formal.",
             abstract = "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 translate three different UML behavioral 
                         diagrams (sequence, behavioral state machines, activity) into a 
                         single Transition System to support Model Checking of UML-based 
                         software. In our approach, properties are formalized based on use 
                         case diagrams. The translation is done for the traditional NuSMV 
                         model checker.",
  conference-location = "S{\~a}o Jos{\'e} dos Campos",
      conference-year = "13-14 nov. 2013",
                label = "lattes: 4896052217878979 1 SantosSantVija:2013:AlTrUM",
             language = "en",
                  ibi = "8JMKD3MGP3W/3FCLDAP",
                  url = "http://urlib.net/ibi/8JMKD3MGP3W/3FCLDAP",
           targetfile = "Santos_algorithm.pdf",
                  url = "http://www.lac.inpe.br/worcap2013/programacao.php",
        urlaccessdate = "03 maio 2024"
}