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. .
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/12409 |
| Date | 23 August 2013 |
| Creators | ANDRADE, Marcelo Costa Melo de |
| Contributors | MOTA, Alexandre Cabral, CORNÉLIO, Márcio Lopes |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | Breton |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.002 seconds