@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 = "04 jun. 2024"
}