Nas últimas décadas constatou-se o uso cada vez mais massivo de sistemas computadorizados principalmente em setores da indústria aeronáutica. Na busca pelo aumento de eficiência no desenvolvimento, recomenda-se o uso do Desenvolvimento Baseado em Modelos (MBD). Este trabalho de pesquisa propõe um Método para Modelagem de Sistemas, denominado M2S, como forma de se bene?ciar da modelagem do sistema desde os estágios iniciais de concepção do sistema. Esta abordagem visa diminuir o ciclo de vida de desenvolvimento e aumentar a qualidade das especi?cações. Nesse sentido, o método proposto se baseia na Linguagem de Modelagem de Sistemas (SysML), no Processo Uni?cado (RUP), no uso de Ambientes Integrados de Engenharia de Software Auxiliada por Computador (I-CASE-E) e na geração automática de código. Após combinar estes elementos num conjunto de passos que compõe o método proposto, realizou-se por meio de um estudo de caso a veri?cação da aplicação do método. O estudo de caso envolveu o desenvolvimento de um protótipo do Sistema de Dados Anemométricos (Air Data System - ADS), com dois experimentos. Foi possível constatar a facilidade em segregar as fases de desenvolvimento, realizar a evolução gradual das especi?cações e modelos, para ?nalmente se chegar a transformação dos modelos independentes de plataforma em código fonte e se constituir o protótipo. Aplicou-se testes e métricas de Halstead, de Linhas de Código e de Complexidade Ciclomática como forma de comparar os dois experimentos.

Um novo modelo para a especificação de hiperdocumentos denominado HMBS - Hyperdocument Model Based on Statecharts - é proposto. O HMBS adota como modelo formal subjacente a técnica Statecharts, cuja estrutura e semântica operacional são utilizadas para especificar a estrutura organizacional e a semântica de navegação de hiperdocumentos grandes e complexos. A definição do HMBS, bem como a semântica de navegação adotada, são apresentadas. Na definição apresenta-se como o modelo permite separar as informações referentes a estrutura organizacional e navegacional das representações físicas do hiperdocumento. Também são discutidas características do modelo que possibilitam ao autor analisar a estrutura do hiperdocumento, encorajando a especificação de hiperdocumentos estruturados. Para provar e validar a viabilidade prática do uso do HMBS num contexto real foi desenvolvido um ambiente de autoria e navegação de hiperdocumentos denominado HySCharts - Hyperdocumenf System based on Statecharts. Esse ambiente fornece facilidades de prototipação rápida e simulação interativa de hiperdocumentos. Para ilustrar como o modelo HMBS e o HySCharts podem ser utilizados no contexto de uma abordagem de projeto sistemática é utilizada como estudo de caso a especificação de um hiperdocumento que apresenta o Parque Ecológico de São Carlos / A new model for hyperdocument specification called HMBS - Hyperdocument Model Based on Statecharts - is proposed. HMBS uses the Statechart formalism as its underlying model. Statecharts structure and operational semantics are used to specify the organizational structure and the browsing semantics of large and complex hyperdocuments. The definition of HMBS is presented and its browsing semantics is described. It is shown how the model allows the separation of information related to the organizational and navigational structure from the hyperdocument\'s physical representation. Model features that allow authors to analyze the hyperdocument structure, encouraging the specification of structured hyperdocuments are also discussed. As a proof of concept and also to evaluate the feasibility of using HMBS in real-life applications a system called HySCharts - Hyperdocument System based on StateCharts - was developed. HySCharts is composed by an authoring and a browsing environments, supporting rapid prototyping and interactive simulation of hyperdocuments. A case study is presented that uses the specification of a hyperdocument introducing the Ecological Park of São Carlos to illustrate the use of HMBS and of the HySCharts environment integrated into a systematic design approach

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. .

É cada vez mais notável o desenvolvimento da indústria micro-eletrônica. A criação de dispositivos eletrônicos menores, que apresentam maior autonomia de energia, aliados ao aumento do poder de processamento, armazenamento e comunicação sem fio de alta velocidade favoreceram o surgimento e disseminação de novas tecnologias e paradigmas, dentre elas a Internet das Coisas (IoT). Do ponto de vista tecnológico, IoT é uma rede de objetos físicos que possuem tecnologia embarcada de sensoriamento e atuação. Agências de consultoria empresarial, tais como a McKinsey & Company, afirmam que IoT apresenta valor de mercado bilionário e poderá ultrapassar a casa dos trilhões antes de 2020. Dessa forma, o mercado de IoT vem se apresentando como um dos mercados mais promissores para os próximos anos. Alguns dos problemas que podem postergar este crescimento são os problemas decorrentes da dificuldade de integração e escalabilidade das aplicações de IoT. Em IoT, problemas de interoperabilidade são corriqueiros, seja pela alta diversidade de dispositivos empregados, seja pela incompatibilidade entre fabricantes. Em relação a escalabilidade, sistemas de IoT possuem uma demanda natural por alta escala, visto que buscam atender demandas comuns a vários setores, seja na indústria, transporte, domótica, segurança pública, comércio, entre outros. Este trabalho apresenta uma solução para esses problemas através do SWoTPAD, um framework formal que auxilia o projetista no desenvolvimento de soluções para IoT. SWoTPAD oferece uma linguagem para especificar dispositivos e serviços, descrever o ambiente e realizar requisições. Adicionalmente, ele gera o módulo de descoberta, composição automática de serviços e execução. Aplicações SWoTPAD são facilmente integráveis, pois usam e estendem um mesmo conjunto de ontologias, o que garante a compatibilidade nos dados gerados e consumidos por essas aplicações. A escalabilidade advém da associação de anotações semânticas a cada um dos elementos que compõem a aplicação de IoT. Essas anotações permitem ao SWoTPAD descobrir, classificar, selecionar e compor automaticamente serviços do ambiente. Dessa forma, SWoTPAD pode procurar por soluções alternativas, quando o serviço original apto a atender uma determinada demanda se encontra sobrecarregado ou indisponível. Para validação do framework, foram adotados dois estudos de caso. O primeiro deles, o problema de implantação de serviços em um ambiente de nuvem, e o segundo, uma aplicação de segurança residencial. O estudo de caso demonstrou que é possível desenvolver aplicações completas de IoT no framework proposto. Adicionalmente, o mecanismo de composição automática gerado pelo framework para essas aplicações apresenta uma piora média de 45% de desempenho quando comparado à composição manual. / The development of the micro-electronics industry is becoming more and more remarkable. The creation of smaller electronic devices, with higher degree of autonomy, processing, storage, and wireless communication favor the emergence and dissemination of new technologies and paradigms, such as the Internet of Things (IoT ). From the technological point of view, IoT is a network of physical objects that have embedded technology of sensing and actuation. McKinsey & Company says the IoT market is already reaching billionaire numbers and may exceed the trillions by 2020. Thus, the IoT market is proving to be one of the most promising markets in the next years. Problems that can delay this growth come from the difficulty of integration and scalability of IoT applications. In IoT, interoperability problems are common, either because of the high diversity of devices used, or because of the incompatibility between manufacturers. Regarding scalability, IoT systems have a natural demand for high scale, since they seek to meet common demands in various sectors, be it in industry, transportation, home automation, public safety, commerce, among others. This work solves these problems through SWoTPAD, a formal framework that assists the designer in developing solutions for IoT. SWoTPAD provides a language for specifying devices and services, describing the environment, and performing requests. Additionally, it generates the discovery, automatic service composition, and execution module. SWoTPAD applications are easily integrable, since they use and extend the same set of ontologies, which guarantees compatibility in the data generated and consumed by these applications. Scalability comes from the association of semantic annotations to each of the elements that compose the IoT application. These annotations allow SWoTPAD to discover, rank, select, and automatically compose services. In this way, SWoTPAD can search for alternative solutions, when the original service able to meet a particular demand is overloaded or unavailable. Two case studies were developed for validation of the framework. The first one, the problem of deploying services in a cloud environment, and the second, a home security system. The case study demonstrated that it is possible to develop complete IoT applications in the proposed framework. Also, the automatic service composition module generated by SWoTPAD for these applications has a mean worsening of 45 % of performance when compared to the manual composition.

Os estudos realizados no presente trabalho de tese abrangem o processo de integração de subsistemas de tempo real intensivos em software e o formalismo de geração de casos de teste. A integração de subsistemas é uma fase altamente onerosa em tempo e recursos de teste de projetos de sistemas críticos tais como plataformas de satélites. São investigados testes baseados em modelos de estado que representam a interação dos subsistemas comunicantes. O problema pesquisado é o formalismo adequado para representar requisitos de tempo no modelo comportamental da interação de modo que casos de teste possam ser derivados por métodos automáticos. Com foco na modelagem dos serviços providos pelos subsistemas em integração, propõe-se um arcabouço para teste de interoperabilidade e de robustez composto por cinco elementos estruturantes: (1) perfil do serviço, (2) modelo nominal do serviço, (3) perigos de tempo, (4) modelo aumentado do serviço, e (5) propósito de teste. O arcabouço, denominado InRob, orienta a construção de modelos formais de interoperabilidade os quais representam o comportamento de um serviço em um dado estágio de integração. Os modelos são estendidos com propriedades de tempo de modo que possam ser derivados casos de teste de robustez, relativos a desvios de tempo na troca de mensagens entre os subsistemas. A validação da abordagem InRob é feita no domínio de subsistemas espaciais, na integração dos subsistemas que compõem um instrumento imageador (telescópio) de raios X a bordo de uma missão de satélite de astronomia. Nesse estudo de caso, o InRob é instanciado em um processo de teste composto por três etapas, duas delas apoiadas por ferramentas existentes para geração e execução de casos de teste.

CCS (Communicating and Concurrent Systems) is the process algebra to specify and verify concurrent and communicating systems. This work proposes a transformation guide of the CCS equations into to the UML-RT (Unified Modeling Language for Real-Time) model and a transformation guide of the UML-RT model into a set of CCS equations. The UML-RT model is a software design language, which supports code generation and the construction of executable systems. The UML-RT is an UML extension, and it does not have a formal semantics; therefore it is not possible to verify UMLRT models. The transformation guide of UML-RT models into CCS equations allows verifying the models. We argue that the transformation of CCS models into UML-RT models allows an alternative way of correctly building systems. This work details the transformation guides from CCS equations to UML-RT models and from UML-RT models to CSS equations and it discusses the limitations and benefits.

É cada vez mais notável o desenvolvimento da indústria micro-eletrônica. A criação de dispositivos eletrônicos menores, que apresentam maior autonomia de energia, aliados ao aumento do poder de processamento, armazenamento e comunicação sem fio de alta velocidade favoreceram o surgimento e disseminação de novas tecnologias e paradigmas, dentre elas a Internet das Coisas (IoT). Do ponto de vista tecnológico, IoT é uma rede de objetos físicos que possuem tecnologia embarcada de sensoriamento e atuação. Agências de consultoria empresarial, tais como a McKinsey & Company, afirmam que IoT apresenta valor de mercado bilionário e poderá ultrapassar a casa dos trilhões antes de 2020. Dessa forma, o mercado de IoT vem se apresentando como um dos mercados mais promissores para os próximos anos. Alguns dos problemas que podem postergar este crescimento são os problemas decorrentes da dificuldade de integração e escalabilidade das aplicações de IoT. Em IoT, problemas de interoperabilidade são corriqueiros, seja pela alta diversidade de dispositivos empregados, seja pela incompatibilidade entre fabricantes. Em relação a escalabilidade, sistemas de IoT possuem uma demanda natural por alta escala, visto que buscam atender demandas comuns a vários setores, seja na indústria, transporte, domótica, segurança pública, comércio, entre outros. Este trabalho apresenta uma solução para esses problemas através do SWoTPAD, um framework formal que auxilia o projetista no desenvolvimento de soluções para IoT. SWoTPAD oferece uma linguagem para especificar dispositivos e serviços, descrever o ambiente e realizar requisições. Adicionalmente, ele gera o módulo de descoberta, composição automática de serviços e execução. Aplicações SWoTPAD são facilmente integráveis, pois usam e estendem um mesmo conjunto de ontologias, o que garante a compatibilidade nos dados gerados e consumidos por essas aplicações. A escalabilidade advém da associação de anotações semânticas a cada um dos elementos que compõem a aplicação de IoT. Essas anotações permitem ao SWoTPAD descobrir, classificar, selecionar e compor automaticamente serviços do ambiente. Dessa forma, SWoTPAD pode procurar por soluções alternativas, quando o serviço original apto a atender uma determinada demanda se encontra sobrecarregado ou indisponível. Para validação do framework, foram adotados dois estudos de caso. O primeiro deles, o problema de implantação de serviços em um ambiente de nuvem, e o segundo, uma aplicação de segurança residencial. O estudo de caso demonstrou que é possível desenvolver aplicações completas de IoT no framework proposto. Adicionalmente, o mecanismo de composição automática gerado pelo framework para essas aplicações apresenta uma piora média de 45% de desempenho quando comparado à composição manual. / The development of the micro-electronics industry is becoming more and more remarkable. The creation of smaller electronic devices, with higher degree of autonomy, processing, storage, and wireless communication favor the emergence and dissemination of new technologies and paradigms, such as the Internet of Things (IoT ). From the technological point of view, IoT is a network of physical objects that have embedded technology of sensing and actuation. McKinsey & Company says the IoT market is already reaching billionaire numbers and may exceed the trillions by 2020. Thus, the IoT market is proving to be one of the most promising markets in the next years. Problems that can delay this growth come from the difficulty of integration and scalability of IoT applications. In IoT, interoperability problems are common, either because of the high diversity of devices used, or because of the incompatibility between manufacturers. Regarding scalability, IoT systems have a natural demand for high scale, since they seek to meet common demands in various sectors, be it in industry, transportation, home automation, public safety, commerce, among others. This work solves these problems through SWoTPAD, a formal framework that assists the designer in developing solutions for IoT. SWoTPAD provides a language for specifying devices and services, describing the environment, and performing requests. Additionally, it generates the discovery, automatic service composition, and execution module. SWoTPAD applications are easily integrable, since they use and extend the same set of ontologies, which guarantees compatibility in the data generated and consumed by these applications. Scalability comes from the association of semantic annotations to each of the elements that compose the IoT application. These annotations allow SWoTPAD to discover, rank, select, and automatically compose services. In this way, SWoTPAD can search for alternative solutions, when the original service able to meet a particular demand is overloaded or unavailable. Two case studies were developed for validation of the framework. The first one, the problem of deploying services in a cloud environment, and the second, a home security system. The case study demonstrated that it is possible to develop complete IoT applications in the proposed framework. Also, the automatic service composition module generated by SWoTPAD for these applications has a mean worsening of 45 % of performance when compared to the manual composition.

Entre as principais dificuldades do desenvolvimento de software embarcado crítico e de tempo real está a especificação e o processo de verificação e validação apoiado ao projeto conceitual. Neste contexto, a modelagem de sistemas tem uma importante função, uma vez que um processo complexo possa ser analisado e validado antes de sua real implementação. Esta dissertação aborda o problema de verificação e validação de software embarcado de um satélite com configuração ACDH (Attitude Control and Data Handling) através de uma plataforma aerosuspensa com um grau de liberdade, utilizando a SysML, a ferramenta CASE TELELOGIC Rhapsody e a orientação das normas da ECSS (European Cooperation on Space Standardization). A partir do modelo obtido, são utilizadas três abordagens para análise e avaliação: (1) Especificação e gerenciamento dos requisitos, através dos conceitos determinados pela ECSS; (2) Modelagem do sistema e verificação dos requisitos, através do formalismo matemático dos autômatos utilizando a técnica de model checking através da ferramenta UPPAL; (3) Conversão do modelo em SysML, aplicando a Engenharia de Requisitos e o processo de verificação e validação do sistema, através da simulação na ferramenta CASE.

Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário. / Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.

Submitted by JÚLIO HEBER SILVA (julioheber@yahoo.com.br) on 2017-04-11T19:28:47Z No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2017-04-12T14:32:03Z (GMT) No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2017-04-12T14:32:03Z (GMT). No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-03-07 / Fundação de Amparo à Pesquisa do Estado de Goiás - FAPEG / The process of developing computer systems takes into account many stages, in which some are more necessary than others, depending on the purpose of the application. The implementation stage is always necessary, indisputably. Sometimes the requirements analysis and testing phases are neglected. And, generally, the part of formal verification correctness is intended for few applications. The use of model checkers has been exploited in the task of validating a behavioral specification in its appropriate level of abstraction, notably specifications validation of critical systems, especially when they involve the preservation of human life, when the existence of errors entails huge financial loss or when deals with information security. Therefore, it proposes to apply formal verification techniques in the validation of the vehicular safety system Avoiding Doored System, considered as critical, in order to verify if the implemented system faithfully meets the requirements for it proposed. For that, it was used as a tool to verify its correctness the Specification and Verification System - PVS, detailing and documenting all the steps employed in the process of specification and formal verification. K / O processo de desenvolvimento de sistemas computacionais leva em conta muitas etapas, nos quais umas são tidas mais necessárias que outras, dependendo da finalidade da aplica- ção. A etapa de implementação sempre é necessária, indiscutivelmente. Por vezes as fases de análise de requisitos e de testes são negligenciadas. E, geralmente, a parte de verifica- ção formal de corretude é destinada a poucas aplicações. O uso de verificadores de modelos tem sido explorado na tarefa de validar uma especificação comportamental no seu nível adequado de abstração, sobretudo, na validação de especificações de sistemas críticos, principalmente quando estes envolvem a preservação da vida humana, quando a existência de erros acarreta enorme prejuízo financeiro ou quando tratam com a segurança da informa- ção. Diante disso, se propõe aplicar técnicas de verificação formal na validação do sistema de segurança veicular Avoiding Doored System, tido como crítico, com o intuito de atestar se o sistema implementado atende, fielmente, os requisitos para ele propostos. Para tal, foi utilizada como ferramenta para a verificação de sua corretude o Specification and Verification System - PVS, detalhando e documentando todas as etapas empregadas no processo de especificação e verificação formal. Pal