@InProceedings{SantosSantVija:2012:FoVeUM,
               author = "Santos, Luciana Brasil Rebelo dos and Santiago J{\'u}nior, 
                         Valdivino Alexandre de and Vijaykumar, Nandamudi Lankalapalli",
          affiliation = "{} and {Instituto Nacional de Pesquisas Espaciais (INPE)} and 
                         {Instituto Nacional de Pesquisas Espaciais (INPE)}",
                title = "Formal verification of UML-based software",
            booktitle = "Anais...",
                 year = "2012",
               editor = "Castro, Ana Paula Abrantes de and Shiguemori, {\'E}lcio Hideiti 
                         and Ramos, Fernando Manuel",
         organization = "Workshop dos Cursos de Computa{\c{c}}{\~a}o Aplicada do INPE, 
                         12. (WORCAP).",
            publisher = "Instituto Nacional de Pesquisas Espaciais (INPE)",
              address = "S{\~a}o Jos{\'e} dos Campos",
             keywords = "formal verification, Model Checking, UML, SOLIMVA methodology.",
             abstract = "ABSTRACT: Formal Verification methods, such as Model Checking, are 
                         best applied in early stages of system design, when costs are low 
                         and benefits can be high, increasing the quality of systems, when 
                         they are completed. The Unified Modeling Language - (UML) is 
                         currently accepted as the de facto standard for modeling 
                         (object-oriented) software, and its use is increasing in the 
                         aerospace industry. This work describes how UML diagrams created 
                         in the early phases of software development, such as sequence, 
                         activity, state machines (variation of Harels Statecharts) 
                         diagrams, can be transformed into a finite-state model to support 
                         Model Checking of UML-based software. The results of this work 
                         will improve SOLIMVA, a methodology initially developed to 
                         generate model-based system and acceptance test cases considering 
                         Natural Language requirements artifacts.",
  conference-location = "S{\~a}o Jos{\'e} dos Campos",
      conference-year = "6-8 nov. 2012",
             language = "en",
         organisation = "Instituto Nacional de Pesquisas Espaciais (INPE)",
                  ibi = "8JMKD3MGP8W/3D85595",
                  url = "http://urlib.net/ibi/8JMKD3MGP8W/3D85595",
           targetfile = "worcap2012_submission_23 - Luciana Brasil Rebelo dos Santos.pdf",
        urlaccessdate = "03 maio 2024"
}