@InProceedings{ErasSantSantVija:2015:ApBaUM,
               author = "Eras, Eduardo R. and Santos, Luciana Brasil Rebelo and Santiago 
                         Junior, 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)} and {Instituto Nacional de Pesquisas 
                         Espaciais (INPE)}",
                title = "Towards a wide acceptance of formal methods to the design of 
                         safety critical software: An approach based on UML and model 
                         checking",
            booktitle = "Proceedings...",
                 year = "2015",
         organization = "International Conference on Computational Science and Its 
                         Applications, 15. (ICCSA)",
             keywords = "Behavioral diagrams, Model Checking, UML, XMITS.",
             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.",
  conference-location = "Banff, Canada",
      conference-year = "22-25 june",
             language = "en",
           targetfile = "eras_towards.pdf",
        urlaccessdate = "28 abr. 2024"
}