Submitted by João Arthur Martins (joao.arthur@ufpe.br) on 2015-03-11T19:12:53Z No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Approved for entry into archive by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-03-13T13:12:01Z (GMT) No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-13T13:12:01Z (GMT). No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2013-08-23 / Requisitos são um dos principais artefatos no desenvolvimento de um sistema. Para sistemas críticos, os requisitos são artefatos obrigatórios para satisfazer critérios de certificações tais como os descritos no guia de certificação DO-178B. Apesar de sua importância, estes artefatos são geralmente descritos informalmente através de linguagem natural. O uso da linguagem natural propicia a descrição de requisitos ambíguos, incompletos e inconsistentes. Para sanar este problema foi definido o método Software Cost Reduction (SCR), que permite a descrição formal de requisitos de forma precisa e relativamente amigável através do uso de tabelas preenchidas com expressões lógicas. Em particular, de forma a nos aproximarmos ainda mais das tecnologias usadas na indústria de sistemas críticos, neste trabalho nosso SCR é o implementado na ferramenta TTM da suíte T-VEC (um conjunto de ferramentas que suporta a sintaxe de SCR e possibilita a geração de vetores de testes e análise de propriedades), a qual é capaz de gerar casos de teste seguindo o guia DO-178B. Além dos requisitos, a certificação do código implementado também é uma obrigação para sistemas críticos e o uso de SCR somente não garante isso. Enquanto o método SCR auxilia na descrição detalhada de requisitos, o ambiente de desenvolvimento baseado em modelos denominado Safety Critical Application Development Environment (SCADE) auxilia na modelagem de software crítico. SCADE é também usado para gerar código certificado de acordo com o DO-178B. Neste trabalho apresentamos como obter modelos SCADE a partir de especificações descritas em SCR através da aplicação de regras de tradução. Com isto obtemos código certificado a partir de requisitos formais em uma única solução. Para aplicar as regras de forma automática, construímos uma ferramenta tradutora usando o framework Stratego/ XT. Por fim, aplicamos nosso tradutor em dois estudos de caso descritos em SCR. Foi feito uso de uma estratégia de verificação baseada em testes para atestar que os modelos SCADE produzidos por nosso tradutor correspondem às descrições em SCR. A estratégia de verificação consiste em usar T-VEC para gerar vetores de testes de acordo com o critério de cobertura MCDC e então aplicar os testes no código C gerado pelo SCADE. Apesar de nosso tradutor não ser provado correto, podemos argumentar indiretamente que o mesmo preserva as propriedades descritas em SCR nos modelos SCADE gerados automaticamente. Quanto a certificação do tradutor, isto fica a cargo de nosso parceiro industrial Embraer S.A. .

Les phases de validation et de vérification (V&V) des systèmes réactifs temps réel critique (de plus en plus complexes) sont très importantes en termes de coût et de temps. Dans ce contexte, toute méthode et outil permettant d'aider à la réalisation des activités de V&V est d'une très grande importance au cours du développement. Le test fonctionnel est le moyen le plus utilisé au cours de ces phases de V&V. Or, les méthodes de test présentent des limites : un test exhaustif est quasiment impossible à réaliser en raison de la taille et de la complexité des systèmes considérés. Dans ce contexte, les enjeux de la maîtrise de l'effort de test (complexité et coût) sont majeurs, mais les exigences de qualité pour ces systèmes sont très grandes. L'effort de test caractérise tout autant l'élaboration des jeux de test que le diagnostic. Dans cette optique, nous avons défini deux méthodologies basées sur les concepts d'analyse de testabilité et les stratégies de test. La première méthodologie permet d'aider à la définition de jeux de test pertinents et à l'analyse de couverture des systèmes réactifs spécifiés dans un formalisme flot de données SCADE dans le contexte AIRBUS. La seconde propose des méthodes d'aide à la vérification (identification de tests pertinents et localisation de composants défectueux au cours diagnostic) de systèmes sur la chaîne d'assemblage finale (FAL) d'un avion AIRBUS.