Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-06-15T20:18:58Z No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-06-18T19:19:46Z (GMT) No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Made available in DSpace on 2018-06-18T19:19:46Z (GMT). No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) Previous issue date: 2018-02-22 / O uso de Geradores Automáticos de Código para Métodos Formais não apenas minimiza esforços na implementação de Sistemas de Software, como também reduz a chance da existência de erros na execução destes Sistemas. Estas ferramentas, no entanto, podem ter faltas em seus códigos-fonte que causam erros na geração dos Sistemas de Software, e então a verificação de tais ferramentas é encorajada. Esta tese de Doutorado visa criar e desenvolver uma estratégia para verificar JCircus, um Gerador Automático de Código de um amplo sub-conjunto de Circus para Java. O interesse em Circus vem do fato de que ele permite a especificação dos aspectos concorrentes e de estado de um Sistema de maneira direta. A estratégia de verificação consiste nos seguintes passos: (1) extensão da Semântica Operacional de Woodcock e prova de que ela é sólida com respeito à Semântica Denotacional existente de Circus na Teoria Unificada de Programação (UTP), que é um framework que permite prova e unificação entre diferentes teorias; (2) desenvolvimento e implementação de uma estratégia que verifica o refinamento do código gerado por JCircus, através de uma toolchain que engloba um Gerador de Sistema de Transições Rotuladas com Predicado (LPTS) para Circus e um Gerador de Modelos que aceita como entrada (I) o LPTS e (II) o código gerado por JCircus, e gera um modelo em Java Pathfinder que verifica o refinamento do código gerado por JCircus. Através da aplicação do passo (2) combinada com técnicas baseadas em cobertura no código fonte de JCircus, nós visamos aumentar a confiabilidade do código gerado de Circus para Java. / The use of Automatic Code Generators for Formal Methods not only minimizes efforts on the implementation of Software Systems, but also reduces the chance of existing errors on the execution of such Systems. These tools, however, can themselves have faults on their source codes that may cause errors on the generation of Software Systems, and thus verification of such tools is encouraged. This PhD thesis aims at creating and developing a strategy to verify the code generation from the Circus formal method to Java Code. The interest in Circus comes from the fact that it allows the specification of concurrent and state-rich aspects of a System in a straightforward manner. The code generation envisaged to be verified is performed by JCircus, a tool that translates a large subset of Circus to Java code that implements the JCSP API. The strategy of verification consists on the following steps: (1) extension of Woodcock’s Operational Semantics to Circus processes and proof that it is sound with respect to the Denotational Semantics of Circus in the Unifying Theories of Programming (UTP), that is a framework that allows proof and unification of different theories; (2) development and implementation of a strategy that refinement-checks the code generated by JCircus, through a toolchain that encompasses (2.1) a Labelled Predicate Transition System (LPTS) Generator for Circus and (2.2) a Model Generator that inputs (I) a LPTS and (II) the code generated by JCircus, and generates a model (that uses the Java Pathfinder code model-checker) that refinement-checks the code generated by JCircus. Combined with coverage-based techniques on the source code of JCircus, we envisage improving the reliability of the Code Generation from Circus to Java.

As técnicas de teste podem ser divididas, num primeiro nível, naquelas baseadas no código (caixa branca) e naquelas baseadas na especificação (caixa preta ou funcionais). Nenhuma delas é completa pois visam a identificar tipos diferentes de defeitos e a sua utilização em conjunto pode elevar o nível de confiabilidade das aplicações. Assim, tornam-se importantes estudos que contribuam para um melhor entendimento da relação existente entre técnicas funcionais e estruturais, como elas se complementam e como podem ser utilizadas em conjunto. Este trabalho está inserido no contexto do projeto PLAVIS (Plataforma para Validação e Integração de Software em Aplicações Espaciais), e tem como objetivo realizar um estudo comparativo entre as técnicas de geração de casos de teste funcionais (baseadas nas especificações formais) e os critérios estruturais baseados em fluxo de controle e fluxo de dados, aplicados nas implementações. Num contexto específico, esse estudo deve fornecer dados de como se relacionam essas duas técnicas (funcional e estrutural) gerando subsídios para sua utilização em conjunto. Num contexto mais amplo - o do projeto PLAVIS - visa a estabelecer uma estratégia de teste baseada em critérios funcionais e estruturais e que possam, juntamente com as ferramentas que dão suporte a eles, compor um ambiente de teste disponível à utilização em aplicações espaciais dentro do INPE / Testing techniques can be divided, in high level, in code-based ones (white box) and specification based ones (black box). None of them are complete as they intend to identify different kinds of faults. The use of them together can increase the application confidence level. Thus, it is important to investigate the relationship between structural testing techniques and functional testing techniques, how they complete themselves and how they can be used together. This paper was developed in the context of the Plavis (PLAtform of software Validation & Integration on Space systems) project. This project provides comparative studies between functional generation testing techniques (based on formal specifications) and structural generation testing techniques, such as control-flow and data-flow criteria, applied in the implementation. In a specific context, this study provides data about the relationship between these techniques and how they can be used together. In the context of the Plavis project, the goal is to provide a testing strategy, based on functional and structural criteria, and a set of tools, composing a testing environment to be used in Space Applications projects, at INPE

A adoção em larga escala de redes de computadores e gerenciadores de banco de dados contribuiu para o surgimento de sistemas de informação complexos. Atualmente, estes sistemas tornaram-se elementos essenciais na vida das pessoas, dando suporte a processos de negócio e serviços corporativos indispensáveis à sociedade, como automação bancária e telefonia. A utilização de componentes na estruturação destes sistemas promove maior qualidade e flexibilidade ao produto e agiliza o processo de desenvolvimento. Entretanto, para que estes benefícios sejam totalmente observados, é fundamental que os provedores de componentes de prateleira projetem especificações precisas, completas e consistentes. Geralmente, as especificações omitem ou negligenciam o comportamento dos componentes nas situações de falha. Desta forma, a utilização de componentes não confiáveis, cujos comportamentos não podem ser inteiramente previstos, compromete seriamente o projeto de sistemas tolerantes a falhas. Uma estratégia para a especificação de componentes tolerantes a falhas é informar a ocorrência de erros através de exceções e realizar a recuperação dos mesmos por rotinas de tratamento correspondentes. A especificação deve separar claramente o comportamento normal do excepcional, destinado à recuperação do erro. Entretanto, em sistemas concorrentes e distribuídos, a especificação apenas deste tratamento local não é suficiente. Uma exceção pode ser lançada em decorrência de erros sistêmicos (i.e. problemas de rede) que afetam todo o sistema. Assim, determinadas exceções devem ser tratadas em nível arquitetural, envolvendo os demais componentes no tratamento. O modelo conceitual de ações Atômicas Coordenadas (ações CA - Coordinated Atomic actions), bastante aplicado na estruturação de sistemas tolerantes a falhas, define um mecanismo geral para a coordenação do tratamento excepcional dos componentes, que cooperam na execução das atividades e competem por recursos compartilhados. Portanto, o modelo de ações CA oferece uma solução potencialmente viável para a especificação do tratamento de exceções em nível arquitetural. Este trabalho propõe um framework para a especificação do tratamento de exceções em nível arquitetural, baseando-se no modelo de aninhamento de ações CA e utilizando a linguagem orientada a eventos CSP (Communicating Sequential Processes). Sua principal característica é prover um protocolo padronizado para a coordenação do tratamento de exceções, que envolve a cooperação dos componentes do sistema. Além disso, é apresentada uma estratégia para a verificação formal dos sistemas na ferramenta FDR (Failure Divergence Refinement), com base no modelo de refinamento por rastros. / The widespread scale adoption of computer networks and database management systems has contributed to the arising of complex information systems. Nowadays, these systems have become essential aspects in the everyday life, supporting business processes and indispensable enterprise services to society such as banking automation and telephony. The usage of components in structuring of these systems promotes higher quality and flexibility to the product and accelerates the software development process. However, in order to fully observe the benefits it is essential that the suppliers of these COTS (commercial off-the-shelf) design precise, complete and consistent specifications. Generally, the specifications omit or neglect the behavior of these components in exceptional situations. Therefore, the usage of untrustworthy components whose behavior cannot be entirely foreseen seriously compromise the design of fault-tolerant systems. One of the strategies used for the specification of fault-tolerant components is to inform the occurrence of errors through exceptions and make its recovering by the correspondent exception handling routines. The specification should separate clearly the normal behavior from the exceptional one, specially designed for error recovery. However, in concurrent and distributed systems, specification of local exception handling is not enough. An exception could be raised as a result of systemic errors (i.e. network errors) which affect the entire system, thus specific types of exceptions should be treated at an architectural level involving all the other components in this handling activity. The conceptual model of Coordinated Atomic (CA) actions, often applied in the structuring of fault-tolerant systems, defines a general mechanism for coordination of exception handling with components that cooperate while executing activities and compete for shared resources. Therefore, the model of CA actions offers a perfectly viable solution for the specification of exception handling at an architectural level. This work proposes a framework for the specification of exception handling at an architectural level, based on the nesting model of CA actions and using the event-oriented language CSP (Communicating Sequential Processes). Its main characteristic is to provide a standardized protocol for coordination of exception handling that involves the cooperation of system components. Moreover, it is presented a formal strategy for system verification using the FDR (Failure Divergence Refinement) tool, based on the traces refinement model.

Orientador: Ricardo de Oliveira Anido / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-10T11:44:38Z (GMT). No. of bitstreams: 1 SoaresJunior_JurandyMartins_M.pdf: 1209765 bytes, checksum: d8d6bebdcb7b65ed4a9fdb7e84508766 (MD5) Previous issue date: 2006 / Resumo: Testar um subsistema embarcado em um sistema complexo, assumindo-se que os demais subsistemas são livres de falhas, é conhecido como teste de conformidade em contexto. A complexidade deste teste reside no fato do subsistema mais externo, conhecido como contexto, ocultar muitas interações e eventos nos quais o sistema embarcado, conhecido como componente, participa. Nas últimas décadas alguns algoritmos foram desenvolvidos para resolver o problema. Muitos deles, no entanto, ignoram as condições nas quais podem ser aplicados. Nesta dissertação estudamos a teoria e os algoritmos relacionados a teste de conformidade e a teste de conformidade em contexto, propomos uma nova abordagem guiada por casos de teste do componente e analisamos as condições necessárias e suficientes para aplicá-Ia. A validação das condições necessárias e suficientes foi feita em estudos de casos com a pilha de protocolos do TCP/IP, com os protocolos HTTP e HTTPS via Proxy e com DHCP via relay-agent. Os algoritmos estudados foram experimentados nas especificações dos protocolos ABP, SCU e TCP / Abstract: Testing a subsystem embedded into a complex system, in which the other subsystems are assumed to be fault-free, is known as confonnance testing in contexto The complexity behind this test resides in the fact that the most external system, known as context, hides many interactions and events in which the embedded subsystem, known as component, participates. In the last decades some algorithms were developed to solve the problem. Many of them, however, ignore the conditions under which they can be applied. In this dissertation we study the theory and the algorithms related to confonnance testing and conformance testing in context, we propose a new approach guided by component's test cases, and we analyze the necessary and sufficient conditions to apply it. The validation of the necessary and sufficient conditions was done in case studies with the TCP/IP protocol stack, with the protocols HTTP and HTTPS . via Proxy, and with DHCP via relay-agent. The algorithms studied were experimented in the specifications of protocols ABP, seu e TCP / Mestrado / Engenharia de Protocolos / Mestre em Ciência da Computação

Made available in DSpace on 2015-04-11T14:03:15Z (GMT). No. of bitstreams: 1 DISSERTACAO MARCELO.pdf: 1313111 bytes, checksum: ddf9a22433355413e807d3bd27951a01 (MD5) Previous issue date: 2008-12-15 / Fundação de Amparo à Pesquisa do Estado do Amazonas / Embedded systems have undeniable relevance in modern society. They have temporal constraints (as long as they are real time ones), power consumption management, size, weight, etc which make their design more complex than the design of their desktop peers. Given the huge number of requirements of all kinds, the high complexity of embedded software as well as the big possibilities of critical damages in case of flaws and, at last, the even bigger pressure of market for new products faster, it make necessary methods which can assure correct, fast but intuitive specification and conception of designs. Considering this, this work aims to provide a method which contribute to the state of art. The goal of the proposed method is to provide an approach which gather an specification of an embedded software in a semi-formal, object-oriented and Industry-accepted notation, which is Unified Modeling (UML), specifically their Sequence Diagram notation which is able to capture dynamic aspects of a system and a mecanism of translation of this notation into a formal one, called SMV, apropriate for being used by the SMV model checker. The goal of the method is also provide an translation scheme of the sequence diagrams into another formal notation, the so called Petri Nets notations. Petri Net notation is well suited to formal verification. Finally, the goal of the method is to provide a mechanism of translation of high level properties queries into formal notation CTL. Property queries are only qualitative. All these functionalities are implemented in a tool called Ambiente de Verificação Formal de Software Embarcado. / Os sistemas embarcados possuem inegável importância na sociedade atual. Eles possuem restrições temporais (quando são de tempo real), de gerência de consumo de energia, tamanho, peso etc que tornam o seu projeto e concepção mais complexos do que os sistemas convencionais. Dado o grande número de requisitos de todos os tipos, a alta complexidade dos softwares embarcados desenvolvidos bem como a grande possibilidade de catástrofes significativas em caso de falha e por fim a grande pressão de mercado por produtos cada vez mais rápido, fazem-se necessários métodos que possam assegurar uma correta, rápida porém intuitiva especificação e concepção dos projetos. Diante disso, o presente trabalho visa prover um método que acrescente ao atual estado da arte. O objetivo do método então é prover uma abordagem que colete uma especificação de software embarcado em uma notação semi-formal, orientada a objetos e amplamente aceita pela Indústria, que é a Unified Modeling Language (UML), especificamente com seu Diagrama de Sequência, o qual é apto para capturar os aspectos dinâmicos de um sistema e um mecanismo de tradução dessa notação para a notação formal SMV, apta a ser utilizada pelo model checker de mesmo nome. O objetivo do método é prover também um esquema de tradução dos diagramas de sequência em UML para uma notação formal, no caso a notação de Redes de Petri, o qual é adequada para verificação formal, gerando saídas de arquivos nos formatos APNN e PNML. O formato APNN é adequado para ser usado no Model Checking Kit (MCK). Por fim, prover um esquema de tradução consultas de propriedade em alto nível para o formato de CTL puro adequado para ser usado no MCK e um programa em SMV e sua especificação 7 em CTL, formatos aptos a serem usados no model checker SMV. A verificação de propriedades é apenas qualitativa, isto é, que verificará apenas propriedades de execução do software embarcado, em oposição às propriedades quantitativas de tempo por exemplo, comuns em softwares de tempo-real. Todas essas funcionalidades são realizadas por uma ferramenta, chamada Ambiente de Verificação Formal de Software Embarcado.

Submitted by Franciele Moreira (francielemoreyra@gmail.com) on 2018-02-15T15:02:41Z No. of bitstreams: 2 Dissertação - Thiago de Almeida Bastos -2018 .pdf: 2834099 bytes, checksum: 20704146dd6e29dc70c067fcbd0011a2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2018-02-16T09:38:12Z (GMT) No. of bitstreams: 2 Dissertação - Thiago de Almeida Bastos -2018 .pdf: 2834099 bytes, checksum: 20704146dd6e29dc70c067fcbd0011a2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-02-16T09:38:12Z (GMT). No. of bitstreams: 2 Dissertação - Thiago de Almeida Bastos -2018 .pdf: 2834099 bytes, checksum: 20704146dd6e29dc70c067fcbd0011a2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2018-01-30 / This master's thesis seeks to contribute to the automation of production lines, and proposes a methodology for the formal verification of flexible manufacturing models by the Petri-PDL tool. The Petri-PDL framework is based on a multimodal logic associated with a scheme defined for the problem with the Petri nets to specify and model sequential problems demonstrating in logical proofs the correctness of properties inferred by the model. This formal treatment is adapted for the treatment of flexible sequential processes, since these models are used in many other applications with Petri nets. They will be considered models of flexible production system found in the systematic review to evaluate the efficiency of its model and its adaptation to this formal refinement. / Este trabalho busca contribuir com a automação de linhas de produção e propõe uma metodologia para a verificação formal de modelos de manufatura flexível a partir da ferramenta Petri-PDL. O conceito Petri-PDL baseia-se em uma lógica multimodal associada ao esquema definido para o problema com as redes de Petri para especificar e modelar problemas sequenciais demonstrando em provas lógicas a corretude de propriedades inferidas pelo modelo. Este tratamento formal será adaptado para o tratamento de processos sequenciais flexíveis, uma vez que estes modelos são usados em muitas outras aplicações com redes de Petri. Serão considerados modelos de sistema de produção flexível encontrados na revisão sistemática para avaliar a eficiência de seu modelo e sua adaptação a este refinamento formal.

As melhores práticas de engenharia de software indicam que a atividade de verificação é fundamental para se alcançar o mínimo de qualidade na construção de um software. Nos processos de desenvolvimento baseados na UML, um dos seus focos principais é detectar inconsistências nos diagramas representativos do software. No entanto, a maioria desses processos, como o Iconix, aplica apenas técnicas informais (ex: inspeções visuais nos modelos), fazendo com que muitas vezes essa atividade seja negligenciada pelos desenvolvedores. Por outro lado, com o avanço das ferramentas automatizadas de verificação, os métodos formais, tais como o Event-B, estão atraindo cada vez mais a atenção das empresas de software. Porém, ainda é difícil convencer os desenvolvedores a adotá-los, pois não estão acostumados com os conceitos matemáticos envolvidos. Assim, este trabalho apresenta uma proposta de inclusão do Event-B no Iconix, dando origem ao BIconix, um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. Mais especificamente, esta tese aborda a tradução automática dos quatro diagramas existentes no Iconix (classes, casos de uso, robustez e sequência) para o Event-B, além de mostrar como esta formalização pode auxiliar na atividade de verificação em pontos específicos e bem definidos no processo proposto. / The best practices of software engineering indicate that the verification activity is essential to achieve some quality during the software construction. In UML-based development processes, one of its main focuses is the detection of inconsistencies in diagrams that represent the software. However, most of these processes, such as Iconix, apply only informal techniques (eg. visual model inspections), often implying the negligence of that activity by developers. Moreover, with the advance of automated verification tools, formal methods, such as Event-B, are increasingly attracting the attention of software companies. However, it is still difficult to convince developers to adopt them, because they are not acquainted with some mathematical concepts. Thus, this paper presents a proposal for the inclusion of Event-B within Iconix, giving rise to BIconix, an object-oriented development process that supports automatic inconsistencies formal verification. More specifically, this thesis addresses the translation of the four existing diagrams in Iconix (classes, use cases, robustness and sequence) to Event- B, and show how this formalization can assist the verification activity in well-defined check points of the proposed process.

Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely re exive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as an MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., \"every time the agent does X, it will do Y later\"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS\'s and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or an inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose with respect to the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again. In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into an MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach. / Sistemas multi-agentes (SMAs) podem ser usados para modelar fenômenos que podem ser decompostos em diversos agentes que interagem entre si dentro de um ambiente. Em particular, eles podem ser usados para modelar sociedades humanas e animais, com a finalidade de se analisar as suas propriedades computacionalmente. Esta tese trata da análise automatizada de um tipo particular de tais modelos sociais, a saber, aqueles baseados em princípios behavioristas, o que contrasta com as abordagens cognitivas mais dominante na literatura de SMAs. A principal característica das teorias behaviorista é a ênfase na descrição do comportamento em termos da interação entre agentes e seu ambiente. Desta forma, não apenas ações refl exivas, mas também de aprendizado, motivações, e as emoções podem ser definidas. Mais especificamente, nesta tese apresentamos uma arquitetura de agentes formal (especificada através da Notação Z) baseada na teoria da Análise do Comportamento de B. F. Skinner, e fornecemos uma noção adequada e formal de ambiente (com base na álgebra de processos pi-calculus) para colocar tais agentes juntos em um SMA. Simulações são freqüentemente utilizadas para se analisar SMAs. As técnicas envolvidas tipicamente consistem em simular um SMA diversas vezes, seja para coletar estatísticas, seja para observar o que acontece através de animações. Contudo, simulações podem ser usadas de forma a pertmitir a realização de verificações automatizadas do SMA caso sejam entendidas como explorações de grandes espaços-de-estados. Nesta tese propomos uma técnica de verificação baseada nessa observação, que consiste em simular um SMA de uma forma guiada, a fim de se determinar se uma dada hipótese sobre ele é verdadeira ou não. Para tal fim, tiramos proveito da importância que os ambientes têm nesta tese: a especificação formal do ambiente de um SMA serve para calcular as evoluções possíveis do SMA como um sistema de transição, estabelecendo assim o espaço-de-estados a ser investigado. Neste cálculo, os agentes são levados em conta simulando-os, a fim de determinar, em cada estado do ambiente, quais são suas ações. Cada execução da simulação é uma seqüência de estados nesse espaço-de-estados, que é calculado em tempo de execução, conforme a simulação progride. A hipótese a ser investigada, por sua vez, é dada como um outro sistema de transição, chamado propósito de simulação, o qual define as simulações desejáveis e indesejáveis (e.g., \"sempre que o agente fizer X, ele fará Y depois\"). Em seguida, é possível verificar se o SMA satisfaz o propósito de simulação de acordo com uma série de relações de satisfatibilidade precisamente definidas. Algoritmicamente, isso corresponde a construir um produto síncrono desses dois sistemas de transições (i.e., o do SMA e o do propósito de simulação) em tempo de execução e usá-lo para operar um simulador. Ou seja, o propósito de simulação é usado para guiar o simulador, de modo que somente os estados relevantes sejam efetivamente simulados. Ao terminar, um tal algoritmo pode fornecer um veredito conclusivo ou inconclusivo. Se conclusivo, descobre-se se o SMA satisfaz ou não o propósito de simulação com relação às observações feitas durante as simulações. Se inconclusivo, é possível realizar alguns ajustes e tentar novamente. em resumo, portanto, nesta tese propomos quatro novos elementos: (i) uma arquitetura de agente, (ii) uma especificação formal do ambiente desses agentes, de modo que possam ser compostos em um SMA, (iii) uma estrutura para descrever a propriedade de interesse, a qual chamamos de propósito de simulação, e (iv) uma técnica para se analisar formalmente o SMA resultante com relação a um propósito de simulação. Esses elementos estão implementados em uma ferramenta, denominada Simulador Formalmente Guiado (FGS, do inglês Formally Guided Simulator). Estudos de caso executáveis no FGS são fornecidos para ilustrar a abordagem.

A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente. / Air traffic management systems evolution is being researched to support air transportation demand growth. An evolution alternative is system automation degree increase. Automated systems need to be as safe as current operating systems. It is possible to analyze system requirements with the application of formal specification and formal verification techniques. In this work, a specification cycle is proposed. The specification cycle is a set of guidelines to use formal method techniques on requirements written in natural language. The specification cycle application expected result is a set of formally verified requirements written in natural language. This cycle is comprised of the following stages: system requirements elicitation and specification pattern classification; requirements mapping to LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formal specification languages; specification formal verification using the NuSMV verifier; formal specification adjustment based on verification results; requirements adjustment based on formal specification adjustment. The proposed guidelines are defined with the Automated Airspace Concept (AAC) formal verification analysis, specification patterns and guidelines for the NuSMV formal verifier use. The expected results are accomplished in the specification cycle application on two study cases. The main contribution of this work is the set of guidelines applied to formulate formally verifiable expressions specified in formal specification languages based on system requirements written in natural language.

As melhores práticas de engenharia de software indicam que a atividade de verificação é fundamental para se alcançar o mínimo de qualidade na construção de um software. Nos processos de desenvolvimento baseados na UML, um dos seus focos principais é detectar inconsistências nos diagramas representativos do software. No entanto, a maioria desses processos, como o Iconix, aplica apenas técnicas informais (ex: inspeções visuais nos modelos), fazendo com que muitas vezes essa atividade seja negligenciada pelos desenvolvedores. Por outro lado, com o avanço das ferramentas automatizadas de verificação, os métodos formais, tais como o Event-B, estão atraindo cada vez mais a atenção das empresas de software. Porém, ainda é difícil convencer os desenvolvedores a adotá-los, pois não estão acostumados com os conceitos matemáticos envolvidos. Assim, este trabalho apresenta uma proposta de inclusão do Event-B no Iconix, dando origem ao BIconix, um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. Mais especificamente, esta tese aborda a tradução automática dos quatro diagramas existentes no Iconix (classes, casos de uso, robustez e sequência) para o Event-B, além de mostrar como esta formalização pode auxiliar na atividade de verificação em pontos específicos e bem definidos no processo proposto. / The best practices of software engineering indicate that the verification activity is essential to achieve some quality during the software construction. In UML-based development processes, one of its main focuses is the detection of inconsistencies in diagrams that represent the software. However, most of these processes, such as Iconix, apply only informal techniques (eg. visual model inspections), often implying the negligence of that activity by developers. Moreover, with the advance of automated verification tools, formal methods, such as Event-B, are increasingly attracting the attention of software companies. However, it is still difficult to convince developers to adopt them, because they are not acquainted with some mathematical concepts. Thus, this paper presents a proposal for the inclusion of Event-B within Iconix, giving rise to BIconix, an object-oriented development process that supports automatic inconsistencies formal verification. More specifically, this thesis addresses the translation of the four existing diagrams in Iconix (classes, use cases, robustness and sequence) to Event- B, and show how this formalization can assist the verification activity in well-defined check points of the proposed process.