Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-08-08T12:10:14Z
No. of bitstreams: 2
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
v_final_assinaturas_branco.pdf: 10378086 bytes, checksum: 35e52eff52531ee36b6a5af5b2a20645 (MD5) / Made available in DSpace on 2016-08-08T12:10:14Z (GMT). No. of bitstreams: 2
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
v_final_assinaturas_branco.pdf: 10378086 bytes, checksum: 35e52eff52531ee36b6a5af5b2a20645 (MD5)
Previous issue date: 2016-03-03 / The increasing complexity of systems has led to increasing difficulty in design. Thestandard approach to development, based on trial and error, with testing used at later stages toidentify errors, is costly and leads to unpredictable delivery times. In addition, for critical systems,for which safety is a major concern, early verification and validation (V&V) is recognised asa valuable approach to promote dependability. In this context, we identify three important anddesirable features of a V&V technique: (i) a graphical modelling language; (ii) formal andrigorous reasoning, and (iii) automated support for modelling and reasoning. We address these points with a refinement technique for SysML supported by tools. SysML is a UML-based language for systems design; it has itself become a de facto standard in the area. There is wide availability of tool support from vendors like IBM, Atego, and Sparx Systems. Our work is distinctive in two ways: a semantics for refinement and for a representative collection of elements from the UML4SysML profile (blocks, state machines, activities, and interactions) used in combination. We provide a means to analyse design models specified using SysML. This facilitates the discovery of problems earlier in the system development lifecycle, reducing time and costs of production. In this work we describe our semantics, which is defined using a state-rich process algebra called CML and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case studies are a leadership-election protocol, a critical component of an industrial application, and a dwarf signal, a device used to control rail traffic. Our contributions are: a set of guidelines that provide meaning to the different modelling elements of SysML used during the design of systems; the individual formal semantics for SysML activities, blocks and interactions; an integrated semantics that combines these semantics with another defined for state machines; and a framework for reasoning using refinement about systems specified by collections of SysML diagrams. / O aumento da complexidade dos sistemas tem levado a um aumento na dificuldade da
atividade de projeto. A abordagem padrão para desenvolvimento, baseada em tentativa e erro,
com testes usados em estágios avançados para identificar erros, é custosa e leva a prazos de
entrega imprevisíveis. Além disto, para sistemas críticos, para os quais segurança é um conceito
chave, Verificação e Validação (V&V) com antecedência é reconhecida como uma abordagem
valiosa para promover confiança. Neste contexto, nós identificamos três características importantes
e desejáveis de uma técnica de V&V: (i) uma linguagem de modelagem gráfica; (ii)
raciocínio formal e rigoroso, e (iii) suporte automático para modelagem e raciocínio.
Nós tratamos estes pontos com uma técnica de refinamento para SysML apoiada por
ferramentas. SysML é uma linguagem baseada na UML para o projeto de sistemas. Ela
tem se tornado um padrão de facto na área. Há uma grande disponibilidade de ferramentas
de fornecedores como IBM, Atego, e Sparx Systems. Nosso trabalho se destaca de duas
maneiras: ao fornecer uma semântica para refinamento e considerar uma coleção representativa
de elementos do perfil UML4SysML (blocos, máquina de estados, atividades, e interações)
usados de forma combinada. Nós fornecemos uma estratégia para analisar modelos de projeto
especificados em SysML. Isto facilita a descoberta de problemas mais cedo durante o ciclo de
vida de desenvolvimento de sistemas, reduzindo tempo e custos de produção.
Neste trabalho nós descrevemos nossa semântica a qual é definida usando uma álgebra
de processo rica em estado chamada CML e implementada em uma ferramenta para geração
automática de modelos formais. Nós também mostramos como esta semântica pode ser usada
para análise baseada em refinamento. Nossos estudos de caso são um protocolo de eleição de
líder, o qual é um componente crítico de uma aplicação industrial, e um sinal anão, o qual é um
dispositivo para controlar tráfego em linhas férreas. Nossas contribuições são: um conjunto de
orientações que fornecem significado para os diferentes elementos de modelagem de SysML
usados durante o projeto de sistemas; as semânticas formais individuais para atividades, blocos e
interações de SysML; uma semântica integrada que combina estas semânticas com outra definida
para máquina de estados; e um arcabouço que usa refinamento para raciocínio de sistemas
especificados por coleções de diagramas SysML.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/17636 |
| Date | 03 March 2016 |
| Creators | LIMA, Lucas Albertins de |
| Contributors | http://lattes.cnpq.br/0005349558315095, IYODA, Juliano Manabu, SAMPAIO, Augusto Cezar Alves |
| Publisher | Universidade Federal de Pernambuco, Programa de Pos Graduacao em Ciencia da Computacao, UFPE, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| 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.0026 seconds