Fechar
Metadados

@PhDThesis{Santos:2015:MeApFo,
               author = "Santos, Luciana Brasil Rebelo dos",
                title = "A methodology to apply formal verification to UML-based software",
               school = "Instituto Nacional de Pesquisas Espaciais (INPE)",
                 year = "2015",
              address = "S{\~a}o Jos{\'e} dos Campos",
                month = "2015-10-02",
             keywords = "UML, formal verification, model checking, SOLIMVA, formal methods, 
                         verifica{\c{c}}{\~a}o formal, m{\'e}todos formais.",
             abstract = "Software development organizations aim to add quality to the 
                         created products, especially those dealing with critical systems, 
                         which require high quality software. Formal Methods offer a large 
                         potential to provide more effective verification techniques. 
                         Besides, 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. 
                         Unified Modeling Language (UML) is widely used for modeling 
                         (object-oriented) software, and its use is increasing in the 
                         aerospace industry. 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 PhD thesis presents an extension of a 
                         methodology called SOLIMVA, initially developed to generate 
                         model-based system and acceptance test cases considering Natural 
                         Language requirements artifacts (SOLIMVA 1.0), and to detect 
                         incompleteness in software specifications by means of Model 
                         Checking (SOLIMVA 2.0). Such an extension generated SOLIMVA 3.0 
                         which transforms up to three different UML behavioral diagrams 
                         (sequence, behavioral state machine, and activity) into a single 
                         Transition System to support Model Checking of software developed 
                         in accordance with UML. In SOLIMVA 3.0, properties are formalized 
                         based on use case models or requirements expressed in pure textual 
                         notation. The translation into the Transition System is done for 
                         the NuSMV model checker, but there is a possibility in using other 
                         model checkers, such as SPIN. A tool, XML Metadata Interchange to 
                         Transition System (XMITS), was developed to automate some steps of 
                         SOLIMVA 3.0 methodology. The approach was applied to two real case 
                         studies (embedded software) related to project under development 
                         at Instituto Nacional de Pesquisas Espaciais (INPE). Defects were 
                         detected within the design of these software systems showing the 
                         feasibility of the methodology. The main contribution of this PhD 
                         thesis is the transformation of a non-formal language (UML) to a 
                         formal language (language of the NuSMV model checker) towards a 
                         greater adoption in practice of Formal Methods in software 
                         development. RESUMO: Organiza{\c{c}}{\~o}es que desenvolvem 
                         software objetivam produzir produtos de software de qualidade, 
                         especialmente aquelas que lidam com sistemas cr{\'{\i}}ticos, 
                         que demandam software de alta qualidade. M{\'e}todos Formais 
                         oferecem grande potencial para prover t{\'e}cnicas de 
                         verifica{\c{c}}{\~a}o mais efetivas. Al{\'e}m disso, 
                         m{\'e}todos de Verifica{\c{c}}{\~a}o Formal, como Model 
                         Checking, s{\~a}o aplicados de maneira mais eficiente nos 
                         est{\'a}gios iniciais do projeto de software, quando os custos 
                         ainda s{\~a}o baixos e os benef{\'{\i}}cios podem ser altos, 
                         aumentando a qualidade dos sistemas de software. A Linguagem de 
                         Modelagem Unificada (UML) {\'e} consideravelmente utilizada para 
                         modelar software (orientado a objetos), e seu uso tem crescido na 
                         ind{\'u}stria aeroespacial. 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. Esta tese de doutorado apresenta uma 
                         extens{\~a}o de uma metodologia chamada SOLIMVA, desenvolvida 
                         inicialmente para gerar casos de teste de sistema e de 
                         aceita{\c{c}}{\~a}o baseados em modelos, considerando requisitos 
                         em Linguagem Natural (SOLIMVA 1.0), e para detectar n{\~a}o 
                         completude em especifica{\c{c}}{\~o}es de software utilizando 
                         Model Checking (SOLIMVA 2.0). Tal extens{\~a}o gerou a SOLIMVA 
                         3.0, a qual transforma at{\'e} tr{\^e}s diferentes diagramas 
                         comportamentais da UML (sequ{\^e}ncia, atividades e m{\'a}quina 
                         de estado) em um {\'u}nico Sistema de Transi{\c{c}}{\~a}o de 
                         Estados para possibilitar a aplica{\c{c}}{\~a}o de Model 
                         Checking em software desenvolvido de acordo com a UML. Na SOLIMVA 
                         3.0, as propriedades s{\~a}o formalizadas baseando-se nos modelos 
                         de casos de uso ou em requisitos expressos em nota{\c{c}}{\~a}o 
                         textual pura. A tradu{\c{c}}{\~a}o para o Sistema de 
                         Transi{\c{c}}{\~a}o de Estados {\'e} feita para a ferramenta de 
                         Model Checking NuSMV, mas existe a possibilidade de se utilizar 
                         outras ferramentas, como por exemplo, SPIN. Uma ferramenta, XML 
                         Metadata Interchange to Transition System (XMITS), foi 
                         desenvolvida para automatizar algumas atividades da metodologia 
                         SOLIMVA 3.0. A abordagem foi aplicada em dois estudos de caso 
                         reais (software embarcado) relacionados a um projeto em 
                         desenvolvimento no Instituto Nacional de Pesquisas Espaciais 
                         (INPE). Foram encontrados defeitos nos projetos desses sistemas de 
                         software, mostrando a viabilidade da metodologia. A principal 
                         contribui{\c{c}}{\~a}o desta tese de doutorado {\'e} a 
                         transforma{\c{c}}{\~a}o de uma linguagem n{\~a}o formal (UML) 
                         para uma linguagem formal (linguagem de entrada da ferramenta de 
                         Model Checking NuSMV), tendo como objetivo uma maior 
                         utiliza{\c{c}}{\~a}o, na pr{\'a}tica, de M{\'e}todos Formais 
                         no processo de desenvolvimento de software.",
            committee = "Carvalho, Solon Ven{\^a}ncio de (presidente) and Santiago 
                         J{\'u}nior, Valdivino Alexandre de (orientador) and Vijaykumar, 
                         Nandamudi Lankalapalli (orientador) and Silveira, F{\'a}bio 
                         Fagundes and Yano, Edgar Toshiro",
           copyholder = "SID/SCD",
         englishtitle = "Uma metodologia para aplicar verifica{\c{c}}{\~a}o formal a 
                         software desenvolvido de acordo com UML",
             language = "en",
                pages = "196",
                  ibi = "8JMKD3MGP3W34P/3K7T2BB",
                  url = "http://urlib.net/rep/8JMKD3MGP3W34P/3K7T2BB",
           targetfile = "publicacao.pdf",
        urlaccessdate = "05 dez. 2020"
}


Fechar