@InProceedings{ErasVija:2014:DiUMVe,
               author = "Eras, Eduardo Rohde and Vijaykumar, Nandamudi Lankalapalli",
          affiliation = "{} and {Instituto Nacional de Pesquisas Espaciais (INPE)}",
                title = "Diagramas UML na verifica{\c{c}}{\~a}o formal de software",
            booktitle = "Anais...",
                 year = "2014",
         organization = "Semin{\'a}rio de Inicia{\c{c}}{\~a}o Cient{\'{\i}}fica do 
                         INPE (SICINPE).",
            publisher = "INPE",
              address = "S{\~a}o Jos{\'e} dos Campos",
                 note = "{Bolsa PIBIC/INPE/CNPq}",
             keywords = "diagramas UML, software.",
             abstract = "M{\'e}todos de Verifica{\c{c}}{\~a}o Formal oferecem grande 
                         potencial para prover t{\'e}cnicas de verifica{\c{c}}{\~a}o 
                         mais efetivas, pois utilizam rigor matem{\'a}tico para 
                         estabelecer a corre{\c{c}}{\~a}o do sistema (BAIER, 2008). 
                         Al{\'e}m disso, M{\'e}todos de Verifica{\c{c}}{\~a}o Formal, 
                         como por exemplo Model Checking, s{\~a}o aplicados de forma mais 
                         eficiente nos est{\'a}gios iniciais do projeto de software, 
                         quando os custos s{\~a}o ainda baixos e os benef{\'{\i}}cios 
                         podem ser altos, aumentando a qualidade dos sistemas de software. 
                         Todavia, exatamente por utilizarem um rigor matem{\'a}tico que 
                         muitas vezes {\'e} exigido dos usu{\'a}rios, M{\'e}todos de 
                         Verifica{\c{c}}{\~a}o Formal n{\~a}o s{\~a}o muito adotados 
                         como t{\'e}cnica de verifica{\c{c}}{\~a}o de sistemas, pois a 
                         prefer{\^e}ncia dos usu{\'a}rios {\'e} dada a processos de 
                         verifica{\c{c}}{\~a}o mais simples. A Linguagem de Modelagem 
                         Unificada (UML) {\'e} atualmente aceita como padr{\~a}o para 
                         modelagem de projeto de software, e seu uso tem crescido na 
                         ind{\'u}stria aeroespacial. UML apresenta diversos diagramas 
                         focando em aspectos distintos do software mas, ao mesmo tempo, 
                         prov{\^e} descri{\c{c}}{\~o}es redundantes dos mesmos aspectos 
                         do sistema. Isso d{\'a} a oportunidade para t{\'e}cnicas de 
                         verifica{\c{c}}{\~a}o e valida{\c{c}}{\~a}o de assegurar a 
                         consist{\^e}ncia das descri{\c{c}}{\~o}es. Contudo, 
                         verifica{\c{c}}{\~a}o e valida{\c{c}}{\~a}o de sistemas 
                         complexos desenvolvidos de acordo com UML n{\~a}o s{\~a}o 
                         tarefas triviais, devido a complexidade do software em si, e a 
                         diversos diagramas/modelos UML diferentes que podem ser usados 
                         para modelar o comportamento e a estrutura do sistema.",
  conference-location = "S{\~a}o Jos{\'e} dos Campos",
      conference-year = "30-31 jul., 2014",
             language = "pt",
                  ibi = "8JMKD3MGP5W34M/3GTNLFH",
                  url = "http://urlib.net/ibi/8JMKD3MGP5W34M/3GTNLFH",
           targetfile = "Eras_diagramas.pdf",
        urlaccessdate = "23 abr. 2024"
}