A methodology to apply formal verification to UML-based software

• Ano de defesa: 2015
• Autor(a) principal: Luciana Brasil Rebelo dos Santos
• Orientador(a): Valdivino Alexandre de Santiago Júnior, Nandamudi Lankalapalli Vijaykumar
• Banca de defesa: Fábio Fagundes Silveira, Edgar Toshiro Yano
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Instituto Nacional de Pesquisas Espaciais (INPE)
• Programa de Pós-Graduação: Programa de Pós-Graduação do INPE em Computação Aplicada
• País: BR
• Link de acesso: http://urlib.net/sid.inpe.br/mtc-m21b/2015/09.08.18.24

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.