Skip navigation
Use este identificador para citar ou linkar para este item: https://repositorio.ufpe.br/handle/123456789/20342

Compartilhe esta página

Título: Transformando modelos Scade em especificações SCR
Autor(es): SERAFIM, Kamila Nayana Carvalho
Palavras-chave: Métodos Formais; Requisitos Formais; Certificação; Regras de Tradução; Testes; Formal Methods; Formal Requirements; Certification; Translation Rules; Tests
Data do documento: 8-Set-2016
Editor: Universidade Federal de Pernambuco
Abstract: A construção de um software para domínios particulares tem de atender normas específicasque impõem o atendimento a fatores como rastreabilidade de requisitos e certificação. Por exemplo, a indústria aeronáutica deve atender à norma DO-178B que estabelece restrições para uso de software de aeronaves, que são considerados sistemas críticos. Para um sistema estar de acordo com essa certificação é necessário ter requisitos formais e código certificado; nesta direção, Andrade (ANDRADE, 2013) usou a notação SCR (Software Cost Reduction) para definição de requisitos e a ferramenta SCADE para modelagem de sistemas críticos, com desenvolvimento de um tradutor de SCR para artefatos xscade. A prática de desenvolvimento de sistema, porém, não está restrita à transição entre requisitos e artefatos de projeto. Modificações realizadas nestes últimos devem também ser refletidas nos requisitos. Neste trabalho desenvolvemos um tradutor de artefatos de modelagem da ferramenta SCADE para SCR. Desta forma podemos gerar especificação de requisitos a partir do código (Engenharia Reversa) e complementamos o trabalho anterior desenvolvido por Andrade (ANDRADE, 2013). Para o desenvolvimento do tradutor, utilizamos a plataforma Spoofax por meio da qual descrevemos a sintaxe do esquema XML utilizado em SCADE e também as regras de tradução tendo como alvo SCR. A validação da tradução teve como ponto de partida o resultado do uso do tradutor desenvolvido por Andrade (ANDRADE, 2013), tendo de gerar como saída a mesma entrada do tradutor desenvolvido por Andrade (ANDRADE, 2013). Além disso, desenvolvemos exemplos para demonstrar que a modificação estrutural, com preservação de semântica, em projetos SCADE, é verificável por meio do uso de testes gerados por meio da ferramenta TTM-TVEC
URI: https://repositorio.ufpe.br/handle/123456789/20342
Aparece nas coleções:Dissertações de Mestrado - Ciência da Computação

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
Dissertação-Transformando-modelos-xscade-em-SCR-Kamila-Serafim.pdf1,1 MBAdobe PDFThumbnail
Visualizar/Abrir


Este arquivo é protegido por direitos autorais



Este item está licenciada sob uma Licença Creative Commons Creative Commons