Made available in DSpace on 2014-06-12T15:59:18Z (GMT). No. of bitstreams: 2 arquivo5011_1.pdf: 1099518 bytes, checksum: 29a36710d81ec239b320f6d900a43fc5 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2004 / Leis de programação são importantes tanto para definir a semântica axiomática de linguagens de programação quanto para auxiliar o processo de desenvolvimento de software. De fato, estas leis podem ser utilizadas como base para práticas informais de desenvolvimento como refactoring, que vem sendo popularizada por metodologias modernas, em especial por Extreme Programming. Embora não tenham sido suficientemente exploradas ainda, as leis de modelagem provavelmente podem trazer benefícios similares, mas com um impacto positivo maior em confiabilidade e produtividade, devido ao melhor suporte antecipado no processo de desenvolvimento de software. Em geral, transformação de modelos que preservam semântica são propostas de maneira ad hoc tendo em vista que são difíceis de serem provadas que são consistentes com respeito a semântica formal. Como consequência, pequenos equívocos podem levar a transformações que deixem o modelo inconsistente. Por estes motivos, este trabalho propõe um conjunto de leis de modelagem (que podem ser vistas como transformações de modelos bidirecionais que preservam semântica) que podem ser utilizas com segurança para se derivar leis mais complexas. Estas leis descrevem transformações de modelos em Alloy, uma linguagem formal para modelagem orientada a objetos. Além disso, será mostrada como estas leis podem ser utilizadas para refatorar especificações em Alloy. Com o intuito de se verificar a consistência das leis, foi proposta uma semântica denotacional para Alloy, utilizando a própria linguagem e uma noção de equivalência indicando quando dois modelos em Alloy possuem a mesma semântica. Por fim, o Alloy Analyzer, ferramenta utilizada para fazer análises em modelos em Alloy, foi estendida com algumas das leis básicas propostas. Como resultado, algumas diretrizes para a implementação de sistemas de transformação foram propostas

Submitted by Kleber Silva (kleberbs@ufba.br) on 2017-02-06T17:13:39Z No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-07T12:02:49Z (GMT) No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Made available in DSpace on 2017-02-07T12:02:49Z (GMT). No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Os Agentes Autônomos – AA e os Sistemas Multiagentes – SMA realizam suas tarefas baseados num planejamento e a sua complexidade vai depender de qual ambiente esteja envolvido, principalmente quando este ambiente é dinâmico e não determinista. A verificação de modelos tem sido aplicada para a verificação de propriedades do planejamento de modo a checar a correção de aplicações baseadas em AAs e SMA’s e tal verificação apresenta muitos desafios para contornar situações potenciais de explosão de estados. O futebol de robôs simulados é uma aplicação que apresenta muitas das características e problemas inerentes aos AA’s e SMA’s como um ambiente não determinista e dinâmico, fato este que vem tornando esta aplicação um relevante estudo de caso para a verificação de modelos de SMA’s. O presente trabalho considera a especificação e verificação de planos de um time de futebol de robôs simulado, o qual é baseado na arquitetura multicamada de Agentes Concorrentes(camada cognitiva, camada instintiva, e camada reativa), utilizando o verificador de modelos UPPAAL. Para atingir os objetivos do trabalho foi proposta uma abordagem incremental e evolutiva para modelar e verificar os planos, a qual inclui abstrações e técnicas baseadas em verificação composicional de modelos (Compositional Model Checking), com o objetivo de contornar situações de explosão de estados. O método proposto também pode ser utilizado em aplicações similares, o qual poderia ser suportado por um ambiente computacional interativo para guiar os analistas no processo de verificação de planos de SMA’s com arquitetura multicamada, usando a verificação de modelos.

Made available in DSpace on 2016-08-29T15:33:24Z (GMT). No. of bitstreams: 1 tese_9681_Ata de Defesa.pdf: 637986 bytes, checksum: 049a7d2723e6d0c1208ad9aad2eb9d0d (MD5) Previous issue date: 2016-03-28 / Um dos problemas clássicos da Teoria de Grafos é o problema de isomorfismo de grafos. Esse problema trata de determinar se, dado dois grafos, é possível definir um mapeamento entre seus vértices de forma que sejam respeitadas as conexões definidas por suas arestas. Um algoritmo proposto recentemente para resolver esse problema é o IVL (Iterated Vertex Labelling) [Baroni (2012)]. O GROOVE (GRaph-based Object-Oriented VErification) é uma ferramenta de verificação de modelos baseados em grafos que faz uso de algoritmos de isomorfismo. No contexto do GROOVE, o problema de isomorfismo de grafos se apresenta de uma maneira diferente do problema clássico: não se deseja determinar se dois grafos são isomorfos, e sim se, dado um grafo, ele é isomorfo a algum dos elementos de um conjunto de grafos. Neste trabalho, propõe-se a adaptação do IVL para o GROOVE e a realiza- ção de experimentos computacionais com o objetivo de determinar se essa adaptação traz ganhos de performance para a ferramenta. Os resultados levam à conclusão de que o IVL tem desempenho análogo ao algoritmo de isomorfismos que já está implementado no GROOVE. Além desses resultados, foi investigado em um cenário similar o uso de filtros de não-isomorfismo, com a intenção de determinar o não-isomorfismo entre dois grafos a um custo computacional baixo. Os resultados dos testes indicam que essa abordagem é bastante promissora, sendo capaz de detectar não-isomorfismos com eficiência de quase 100% , com tempos de execução bem mais baixos que os performados pelo algoritmo atual do GROOVE quando executado nesse cenário adaptado. / The graph isomorphism is a classical problem in Graph Theory, which consists of determining if, given two graphs, it is possible to define a mapping between their vertexes in a way so that the connection defined by their edges are respected. An algorithm proposed recently to solve this problem is the IVL (Iterated Vertex Labelling) [Baroni (2012)]. GROOVE (GRaph-based Object-Oriented VErification) is a graph-based model checking tool which makes use of isomorphism algorithms. In GROOVE’s context, the graph isomorphism problem is set differently from the classical problem: they are not interested on determining if two graphs are isomorphic, instead, they want to determine if, given a graph, it is isomorphic to one of the elements of a graph set. In this work, it’s proposed the IVL adaptation to GROOVE and computational experiments in order to test if this new adapted algorithm brings performance gains to the tool. It can be concluded from the results that IVL has a similar performance compared to the current implementation in GROOVE. Beyond those results, it was investigated in a similar framework the use of non-isomorphism filters, intending to determine the non-isomorphism between two graphs in a low computational cost. The test results point out that this is a promising approach, being able to detect non-isomorphisms with almost 100% efficiency, with a much lower running time when compared to current GROOVE algorithm when executed in this framework.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-23T13:23:08Z No. of bitstreams: 1 DANIEL AGUIAR DA SILVA - DISS PPGCC 2006..pdf: 730843 bytes, checksum: e5d7ebe87ab82d200f68fb0b5b0df784 (MD5) / Made available in DSpace on 2018-08-23T13:23:08Z (GMT). No. of bitstreams: 1 DANIEL AGUIAR DA SILVA - DISS PPGCC 2006..pdf: 730843 bytes, checksum: e5d7ebe87ab82d200f68fb0b5b0df784 (MD5) Previous issue date: 2006-05-26 / Técnicas e ferramentas de testes formais baseados em modelos têm sido desenvolvidas para tornar mais rigoroso e eficiente o processo de teste de sistemas reativos com características de distribuição e concorrência. O não-determinismo inerente a estes sistemas torna os difíceis de serem testados, devido à alta complexidade de obtenção das configurações necessárias para execução dos casos de teste. As propriedades especificadas para estes sistemas são a base para a geração dos casos de teste de conformidade, que devem avaliar a correspondência entre modelo e código. Estas propriedades, denominadas objetivos de teste, devem ser especificadas de maneira a guiar a geração dos casos de teste. Entretanto, a especificação dos objetivos de teste a partir de modelos complexos como os destes sistemas ainda carece de técnicas e ferramentas apropriadas, tornando esta atividade propensa a erros. Os casos de teste podem assim, ter efetividade afetada em caso de erros na especificação dos objetivosdeteste. Comoobjetivodecontribuirparaasoluçãodesteproblema,estetrabalho apresenta técnica de geração de objetivos de teste para sistemas reativos, baseando-se na técnica de verificação de modelos CTL. A técnica proposta visa usufruir da eficiência dos algoritmos da verificação de modelos, por meio de sua adaptação para a análise destes, para a geração dos objetivos de teste. / Techniques and tools for model based testing have been developed to make the process of testing distributed concurrent reactive systems more efficient and rigorous. The inherent nondeterminism of these systems can make it difficult to test them due to the complex process of obtaining test cases configurations from models. To better guide the testing process, properties specified to these systems are used as basis for the test case generation. Such properties, called test purposes, shall be exhibitedby the implementation under test through test case execution. However, specifying test purposes from the common complex and large models of these systems suffers from the lack of appropriated tools and techniques, making it error-prone and inadequate. Thus, test cases based on such test purposes may be affected, getting no desirable soundness. Aiming at solving this problem, we present a technique for test purpose generation for reactive systems based on the CTL model checking technique. We aim at taking benefit from the efficiency of model checking algorithms to better analyze the models to generate the test purposes.

Verificação de modelos é uma das mais eficientes técnicas de verificação automática de sistemas. No entanto, apesar de poder lidar com verificações complexas, as ferramentas de verificação de modelos usualmente não fornecem informação alguma sobre como reparar inconsistências nestes modelos. Nesta dissertação, mostramos que abordagens desenvolvidas para a atualização de modelos CTL inconsistentes não são capazes de lidar com todos os tipos de alterações em modelos. Introduzimos então o conceito de revisão de modelos: uma abordagem baseada em revisão de crenças para o reparo de modelos inconsistentes em um contexto estático. Relacionamos nossa proposta com trabalhos clássicos em revisão de crenças. Definimos um operador de revisão de modelos e mostramos que este obedece postulados de racionalidade clássico de revisão de crenças. Propomos um algoritmo de revisão com base no algoritmo utilizado pela abordagem de atualização de modelos. Discutimos sobre problemas e limites do algoritmo proposto, e mostramos que essa estratégia de adaptação não é uma solução apropriada. / Model checking is one of the most robust techniques in automated system verification. But, although this technique can handle complex verifications, model checking tools usually do not give any information on how to repair inconsistent system models. In this dissertation, we show that approaches developed for CTL model update cannot deal with all kinds of model changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context. We relate our proposal to classical works on belief revision. We define an operator for model revision and we show that it obeys the classical rationality postulates of belief revision. We propose an algorithm for model revision based on the algorithm used by the model update approach. We discuss problems and limitations of our proposed algorithm and show that this strategy of adaptation is not an appropriate solution.

Neste trabalho apresentamos uma implementação de revisão de crenças baseada em comparação de modelos (estados) em uma ferramenta de verificação automática de sistemas de estados finitos. Dada uma fórmula (na lógica CTL) inconsistente com o modelo do sistema, revisamos esse modelo de tal maneira que essa fórmula temporal se torne verdadeira. Como temos oito operadores temporais (AG, AF, AX, AU, EG, EF, EX e EU), foram criados algoritmos especícos para cada um deles. Como o modelo do sistema deriva do seu código na linguagem SMV, a sua revisão passa obrigatoriamente por mudanças na sua descrição. A nossa implementação contempla três tipos de mudanças: acréscimo de linhas, eliminação de linhas e mudança no estado inicial, sendo que as duas primeiras provocam modicações nas transições entre os estados que compõe o modelo. Alguns testes foram aplicados para comprovar a contribuição da revisão de crenças (revisão de modelos) como ferramenta de auxílio ao usuário durante o processo de modelagem de sistemas. / In this work we present an implementation of belief revision based on comparison of models (states) in a tool for automatic verication of nite state systems. Given a formula (in the language of CTL) inconsistent with the model of the system, we revise this model in such way that the temporal formula becomes valid. As we have eight temporal operators (AG, AF, AX, AU, EG, EF, EX and EU), specic algorithms for each one of them have been created. As the model of the system is related with its code in SMV language, its revision forces changes in its description. Our implementation contemplates three types of change: addition of lines, elimination of lines and change in the initial state, where the rst two cause modications in the transitions between the states of the model. Some tests were applied to prove the contribution of the belief revision (model revision) as aid-tool to the user during the process of systems modeling.

Uma importante etapa do desenvolvimento de software é o de levantamento e análise dos requisitos. Porém, durante esta etapa podem ocorrer inconsistências que prejudicarão o andamento do projeto. Além disso, após finalizada a especificação, o cliente pode querer acrescentar ou modificar as funcionalidades do sistema. Tudo isso requer que a especificação do software seja revista, mas isso é altamente custoso, tornando necessário um processo automatizado para simplificar tal revisão. Para lidar com este problema, uma das abordagens utilizadas tem sido o processo de Revisão de Crenças, juntamente com o processo de Verificação de Modelos. O objetivo deste trabalho é utilizar o processo de revisão de crenças e verificação de modelos para avaliar especificações de um projeto procurando inconsistências, utilizando o fragmento universal da Computation Tree Logic (CTL), conhecido como ACTL, e revisá-las gerando sugestões de mudanças na especificação. A nossa proposta é traduzir para lógica clássica tanto o modelo (especificação do software) quanto a propriedade a ser revisada, e então aplicar um resolvedor SAT para verificar a satisfazibilidade da fórmula gerada. A partir da resposta do resolvedor SAT, iremos gerar sugestões válidas de mudanças para a especificação, fazendo o processo de tradução reversa da lógica clássica para o modelo original. / The objective of this work is to join the proccess of belief revision and model checking to evaluate project specifications looking for inconsistences, using the universal fragment of Computation Tree Logic (CTL), known as ACTL, and revise them generating changes suggestions in the specification. Our approach will translate the model (software specification) and the property to be revised to classical logic. Then we will apply a SAT solver to verify the generated formulas satsifability. From the SAT solver answer, we will create changes valid suggestions to the specification making the translation back from classical logic to the original model. To generate the changes suggestions, we proposed a framework based on heuristics where different approaches and decisions can be implemented, aiming a better application for each project scope. We implemented a basic heuristic as an example and used it to test the implementation to analise the proposed algorithm

O uso de aeronaves não tripuladas (VANTs) tem crescido substancialmente nos últimos anos, tanto no campo militar quanto no civil. Roadmaps preveem que em um futuro próximo essas aeronaves compartilhem o espaço aéreo com aeronaves convencionais, exigindo novas arquiteturas de sistemas embarcados que possam garantir uma operação coordenada e segura desses robôs. A maior parte das suas missões baseia-se fortemente em um conjunto de sensores transportados pela aeronave como parte da payload da missão. Contudo, não é trivial a integração de diferentes missões em diferentes aeronaves, visto que ainda não há uma padronização para a comunicação nesses robôs. Para possibilitar essa associação foi proposto neste trabalho a criação de um middleware. Para que se pudesse entender sobre a área de conhecimento dos VANTs realizou-se uma pesquisa sobre esses veículos e suas aplicações e então um protocolo chamado Smart Sensor Protocol (SSP) foi modelado, utilizando-se de técnicas formais para isso. O comportamento do protocolo está modelado com diagrama de estados, seguindo uma gramática escrita utilizando a forma BNF. Este modelo foi verificado com a ferramenta UPPAAL e sua implementação testada em placas Arduino. Os resultados dos testes mostraram que o modelo é viável para o ambiente de embarcados críticos visto que ele provê as funcionalidades necessárias neste cenário sem acrescentar um overhead na comunicação / UNMANNED Aerial Vehicles applications have grown substantially in recent years, both in military and civil fields. Roadmaps predict that in the near future these aircrafts will share the airspace with the conventional planes, requiring new architectures for embedded systems which may ensure a coordinated and safe operation. Most of its tasks are mainly based on a set of sensors carried by the aircraft as part of its payload. However, it is not trivial to integrate different missions in different aircraft plataforms, since there is no standardization for communication in such robots yet. To enable this type of association it was proposed in this masters project the designing of a middleware. It has been carried out a bibliographic review to find out the state-of-the-art in such field, including the specific applications in UAVs, and then a protocol has been modeled following formal techniques. This protocol is called Smart Sensor Protocol (SSP). The SSPs behavior was modeled through state diagrams according to a grammar described using BNF form. This model was verified with the UPPAAL tool and its implementation was run and tested on Arduino boards. The test results pointed out that the model is feasible for critical embedded environments since it provides the necessary functionality in this scenario without addition of an overhead in its communication

Propõe-se uma estratégia de modelagem e de análise formal de políticas de segurança para sistemas baseados em fluxos de trabalho (workflows) e contendo regras que envolvam aspectos de lógica de negócios. Verifica-se com o auxílio de uma política de exemplo que a estratégia proposta resulta em modelos amplamente capazes de expressar restrições lógicas em função de parâmetros de negócio sem comprometer a viabilidade de suas análises. A modelagem baseia-se no uso de um metamodelo definido a partir da identificação das entidades que caracterizam o estado de proteção de um sistema e representado na forma de uma rede de Petri colorida. Por meio da escrita de predicados para consulta sobre o espaço de estados da rede de Petri, verifica-se o atendimento às regras de segurança no modelo formal. A tratabilidade da análise é garantida pela adoção de um paradigma diferenciado principalmente pela busca de ramos inseguros em vez de nós inseguros no espaço de estados e por explorar a natureza independente entre serviços de negócio distintos, expressa por restrições ao fluxo de informação no metamodelo. Tais restrições permitem que a análise seja fracionada evitando o problema da explosão de estados. O exemplo discutido de modelagem e análise de um sistema de serviços bancários online fornece evidências suficientes para atestar a aplicabilidade do método à validação de políticas de segurança para sistemas reais. / A strategy is proposed for the formal modeling and analysis of workflow- -based security policies having rules which involve aspects of business logic. Aided by an example of security policy, the proposed strategy is shown to lead to models widely capable of expressing logical restrictions as functions of business parameters without compromising the feasibility of its analyses. The modeling is based on the usage of a metamodel defined from the identification of the entities that characterize the protection state of a system, and represented as a colored Petri net. By writing predicates for querying the Petri net state-space, compliance with security rules at the formal model is verified. The feasibility of the analysis is ensured by the adoption of a paradigm distinguished mainly for the search for insecure branches rather than insecure nodes in the state-space, and for exploiting the independent nature among different business services, expressed by restrictions to the information flow within the metamodel. Such restrictions allow the analysis to be fractioned, avoiding the state explosion problem. The example provided of modeling and analysis of an online banking services system offers enough evidence to attest the applicability of the method to the validation of security policies for real-world systems.

Planejamento sob incerteza vem sendo cada vez mais requisitado em aplicações práticas de diversas áreas que eequerem soluções confiáveis para metas complexas. Em vista disso, nos últimos anos, algumas abordagens baseadas no uso de métodos formais para síntese automática de planos têm sido propostas na área de Planejamento em Inteligência Artificial. Entre essas abordagens, planejamento baseado em verificação de modelos tem se mostrado uma opção bastante promissora; entretanto, conforme observamos, a maioria dos trabalhos dentro dessa abordagem baseia-se em CTL e trata apenas problemas de planejamento para metas de alcançabilidade simples (como aquelas consideradas no planejamento clássico). Nessa tese, introduzimos uma classe de metas de planejamento mais expressivas (metas de alcançabilidade estendidas) e mostramos que, para essa classe de metas, a semântica de CTL não é adequada para formalizar algoritmos de síntese (ou validação) de planos. Como forma de contornar essa limitação, propomos uma nova versão de CTL, que denominamos alpha-CTL. Então, a partir da semântica dessa nova lógica, implementamos um verificador de modelos (Vactl), com base no qual implementamos também um planejador (Pactl) capaz de resolver problemas de planejamento para metas de alcançabilidade estendidas, em ambientes não-determinísticos com observabilidade completa. Finalmente, discutimos como garantir a qualidade das soluções quando dispomos de um modelo de ambiente onde as probabilidades das transições causadas pela execução das ações são conhecidas. / Planning under uncertainty has being increasingly demanded for practical applications in several areas that require reliable solutions for complex goals. In sight of this, in the last few years, some approaches based on formal methods for automatic synthesis of plans have been proposed in the area of Planning in Artificial Intelligence. Among these approaches, planning based on model checking seems to be a very attractive one; however, as we observe, the majority of the works in this approach are mainly based on CTL and deals only with planning problems for simple reachability goals (as those considered in classical planning). In this thesis, we introduce a more expressive class of planning goals (extended reachability goals) and show that, for this class of goals, the CTL\'s semantics is not adequate to formalize algorithms for synthesis (or validation) of plans. As a way to overcome this limitation, we propose a new version of CTL, called alpha-CTL. Then, based on the semantics of this new logic, we implement a model checker (Vactl), based on which we also implement a planner (Pactl) capable of solving planning problems for extended reachability goals, in nondeterministic planning environments with complete observability. Finally, we discuss how to guarantee the quality of the solutions when we have an environment model where the actions transitions probabilities are known.