Spelling suggestions: "subject:"[een] MODEL CHECKING"" "subject:"[enn] MODEL CHECKING""
201 |
Planejamento sob incerteza para metas de alcançabilidade estendidas / Planning under uncertainty for extended reachability goalsSilvio do Lago Pereira 05 November 2007 (has links)
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.
|
202 |
A refinement based strategy for locally verifying networks of CSP processesANTONINO, Pedro Ribeiro Gonçalves 31 March 2014 (has links)
The increase of computer systems complexity has led to a direct increase in the difficulty of
verifying their correctness. For mastering this complexity, formal methods can be used in
the development of systems providing techniques for both design and verification. Regarding
concurrent and distributed systems, the necessity of a formal approach is more prominent given
the substantial increase in complexity due to the countless number of interactions between
their constituent systems. Unfortunately, however, current methods are not capable of dealing
with the automated analysis of such systems in general, even if we consider only classical
properties such as deadlock freedom; the state explosion problem is the main reason for this
ineffectiveness.
This work is a contribution in this direction. Particularly, considering networks of CSP processes,
this work proposes a local strategy for deadlock analysis based on the notion of process
refinement. The locality of this strategy prevents the state explosion problem generated by the
interaction of constituent systems, which represents a major asset of our strategy. We define a
refinement assertion for checking conflict freedom between pairs of processes in the network;
this can be used for the local verification of networks with an acyclic communication topology.
Concerning networks with a cyclic communication topology, we propose three patterns
that prevent deadlocks: the resource allocation, the client/server and the async dynamic. These
patterns impose behavioural and structural restrictions to prevent deadlocks. The behavioural
restrictions are also captured by refinement assertions, which enable one to automatically verify
these conditions using a refinement checker.
Besides this, we develop four case studies to evaluate the efficiency of our strategy in practice:
a ring buffer, a dining philosopher, and two variations of a leadership election algorithm.
One of the variations of the leadership election algorithm consists of a model used in practice by
the B&O Company, an industrial partner. In this study, we compare our strategy with two other
techniques for deadlock freedom verification, the SSD algorithm of the Deadlock Checker tool
and the built-in deadlock freedom assertion of FDR. This study demonstrates how our strategy
can be used and that it might be a useful alternative to analysing complex industrial systems for
deadlock freedom. / Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-10T16:54:41Z
No. of bitstreams: 2
DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-11T17:34:41Z (GMT). No. of bitstreams: 2
DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
Previous issue date: 2014-03-31 / Com o aumento da complexidade dos sistemas computacionais, houve também um aumento da
dificuldade na tarefa de verificação de sistemas. Para lidar com essa complexidade, métodos
formais podem ser usados no desenvolvimento de sistemas, fornecendo técnicas para a modelagem
e verificação. No contexto de sistemas concorrentes e distribuídos, a necessidade de uma
abordagem formal é ainda mais proeminente, dadas as inúmeras possibilidades de interação entre
seus sistemas componentes. Entretanto, infelizmente, os métodos atuais não se encontram,
de forma geral, completamente aptos a lidar com a análise automática desses sistemas, mesmo
em se tratando de propriedades clássicas como a ausência de deadlocks. A explosão do espaço
de estados a ser analisado é o principal fator para essa ineficácia por parte desses sistemas.
O trabalho apresentado é uma contribuição nesta direção. Considerando o conceito de redes
de processos CSP, o presente trabalho propõe uma estratégia local para a análise de deadlocks
baseada na noção de refinamento de processos. A localidade dessa estratégia previne a explosão
de espaço de estados causada pela interação de sistemas componentes, o que constitui uma
vantajosa característica da nossa estratégia. O trabalho define uma expressão de refinamento
capturando o conceito de ausência de conflito, que pode ser usado para verificar localmente que
uma rede de processos com uma topologia de comunicação acíclica é livre de deadlocks. Para
as redes com topologia cíclica, o trabalho sistematiza e formaliza três padrões comportamentais
que impedem deadlocks: o alocação de recursos, o cliente/servidor e o assíncrono dinâmico.
Esses padrões impõem restrições comportamentais e estruturais para prevenir deadlocks. Essas
restrições comportamentais também são capturadas através de expressões de refinamento,
o que possibilita a verificação automática dessas condições com o uso de um verificador de
refinamento.
Além disso, são apresentados quatro estudos de caso usados para avaliar o desempenho da
nossa técnica na prática: um buffer circular, um jantar dos filósofos e duas variações de um
algoritmo para eleição de líder. Uma dessas variações consiste num modelo usado na prática
pela empresa B&O, um parceiro industrial. Nesse estudo, avaliamos a nossa técnica em comparação
com outras duas técnicas para verificação de ausência de deadlocks, o algoritmo SSD
da ferramenta Deadlock Checker e a asserção de verificação de deadlocks padrão do verificador
de modelos FDR. Esse estudo demonstra como a nossa estratégia é aplicada e que ela pode ser
uma alternativa vantajosa para a verificação de sistemas complexos.
|
203 |
Abstraction of infinite and communicating CSPZ processesFARIAS, Adalberto Cajueiro de 31 January 2009 (has links)
Made available in DSpace on 2014-06-12T15:49:26Z (GMT). No. of bitstreams: 1
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2009 / Esta tese trata de um problema muito comum em verificação formal: explosão de estados.
O problema desabilita a verificação automática de propriedades através da verificação de
modelos. Isto é superado pelo uso de abstração de dados, em que o espaço de estados de
umsistema é reduzido usandoumprincípio simples: descartando detalhes de tal forma que
o espaço de estados torna-se finito exibindo ainda propriedades desejáveis. Isso habilita o
uso de verificacao de modelos, já que o modelo mais simples (abstrato) pode ser usado no
lugar do modelo original (concreto). Entretanto, abstrações podem perder propriedades já
que o nível de precisão é degradado, para algumas propriedades.
Abstrair tipos de dados é, normalmente, uma tarefa não-trivial e requer uma profunda
experiência: o usuário deve prover domínios abstratos, uma relacao matemática entre os
estados (concreto e abstrato), uma inicialização abstrata, e uma versão abstrata para cada
operação. A abordagem proposta nesta tese transfere a maior parte dessa experiência para
um procedimento sistemático que calcula relações de abstração. Essas relações são a base
para as relações matemáticas entre os estados, como também suas imagens determinam os
domínios abstratos (os valores de dados mínimos para preservar propriedades). Também
propomos meta-modelos para estabelecer como o sistema abstrato é inicializado e como
operações são tornadas fechadas sob os domínios abstratos. Isso elimina o conhecimento
requerido do usuário para fornecer as versões abstratas para a inicialização e operações. Os
meta-modelos garantem a correspondência entre os sistemas concreto e abstrato. Assim,
nós derivamos especificações abstratasa partir de concretas de tal formaque a especificação
concreta é mais determinística que a abstrata por construção. Esta é a idéia por trás da teoria
sobrejacente de nossa abordagem de abstração de dados: refinamento de dados.
A notação adotada é CSPZ uma integração formal das linguagens de especificação CSP
e Z. Uma especificação CSPZ tem duas partes: uma parte comportamental (CSP) e outra de
dados (Z). O procedimento de cálculo foca na parte de Z, mas os resultados são usados na
especificação CSPZ por completo; isso segue da independência de dados da parte de CSP (os
dados não podem afetar seu comportamento). Ao final, a verificação automática é obtida
pela conversão da especificação CSPZ em CSP puro e em seguida pelo reuso do verificador
de modelos padrão de CSP.
Nossa abordagem compreende as seguintes tarefas: nós extraímos a parte de Z de uma
especificação CSPZ (puramente sintática), calculamos as relações de abstração (através de
uma análise sistemática de predicados com uso de ferramenta de suporte), construímos as
relações matemáticas entre os estados, os esquemas abstratos (definidos por meta-modelos),
e realizamos um pós-processamento na especificação abstrata. A última tarefa pode resultar
em alguns ajustes nas relações de abstração. A novidade prática e maior contribuição de
nossa abordagem é o cálculo sistemático das das relações de abstração, que são os elementos chave de todas abordagens de abstração de dados que estudamos ao longo dos últimos
anos. O refinamento de dados entre o sistema produzido por nossa abordagem e o original
(concreto) é a segunda contribuição deste trabalho.
O procedimento sistemático é na verdade uma técnica de análise de predicado que usa
as restrições sobre os dados para determinar seus valores mínimos que são suficientes para
preservar o comportamento do sistema. Isso evita a execução (concreta ou simbólica) do
sistema analisado. Os passos produzem mapeamentos que revelam alguns elementos cruciais:
o espaço de estados abstrato e as relações matemáticas entre ele e o espaço de estados
concreto. Essas relações são usadas para construir o sistema abstrato seguindo o formato
estabelecido pelos meta-modelos. As limitações de nossa abordagem são também discutidas.
Nós aplicamos a abordagem a alguns exemplos também analisados por outras técnicas
da literatura. Discutimos também sobre trabalhos relacionados procurando destacar
vantagens, desvantagens e aspectos complementares. Finalmente, apresentamos nossas
conclusões e futuras direções para este trabalho
|
204 |
Evaluation of GUI testing techniques for system crashing: from real to model-based controlled experimentsBERTOLINI, Cristiano 31 January 2010 (has links)
Made available in DSpace on 2014-06-12T15:54:24Z (GMT). No. of bitstreams: 2
arquivo7096_1.pdf: 2072025 bytes, checksum: ca8b71b9cfdeb09118a7c281cafe2872 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2010 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Aplicações para celular estão se tornando cada vez mais complexas, bem como testá-las.
Teste de interfaces gráficas (GUI) é uma tendência atual e se faz, em geral, através da
simulação de interações do usuário. Várias técnicas são propostas, no qual, eficiência
(custo de execução) e eficácia (possibilidade de encontrar bugs) são os aspectosmais cruciais
desejados pela industria. No entanto, avaliações mais sistemáticas são necessárias
para identificar quais técnicas melhoram a eficiência e eficácia de tais aplicações. Esta
tese apresenta uma avaliação experimental de duas técnicas de testes de GUI, denominadas
de DH e BxT, que são usadas para testar aplicações de celulares com um histórico
de erros reais. Estas técnicas são executadas por um longo período de tempo (timeout de
40h, por exemplo) tentando identificar as situações críticas que levam o sistema a uma
situação inesperada, onde o sistema pode não continuar sua execução normal. Essa situação
é chamada de estado de crash. A técnicaDHjá existia e é utilizadapela industriade
software, propomos outra chamada de BxT. Em uma avaliação preliminar, comparamos
eficácia e eficiência entre DH e BxT através de uma análise descritiva. Demonstramos
que uma exploração sistemática, realizada pela BxT, é uma abordagem mais interessante
para detectar falhas em aplicativos de celulares. Com base nos resultados preliminares,
planejamos e executamos um experimento controlado para obter evidência estatística
sobre sua eficiência e eficácia. Como ambas as técnicas são limitadas por um timeout
de 40h, o experimento controlado apresenta resultados parciais e, portanto, realizamos
uma investigação mais aprofundada através da análise de sobrevivência. Tal análise permite
encontrar a probabilidade de crash de uma aplicação usando tanto DH quanto BxT.
Como experimentos controlados são onerosos, propomos uma estratégia baseada em experimentos
computacionais utilizando a linguagem PRISM e seu verificador de modelos
para poder comparar técnicas de teste de GUI, em geral, e DH e BxT em particular. No
entanto, os resultados para DH e BxT tem uma limitação: a precisão do modelo não é
estatisticamente comprovada. Assim, propomos uma estratégia que consiste em utilizar
os resultados anteriores da análise de sobrevivência para calibrar nossos modelos. Finalmente,
utilizamos esta estratégia, já com os modelos calibrados, para avaliar uma nova
técnica de teste de GUI chamada Hybrid-BxT (ou simplesmente H-BxT), que é uma
combinação de DH e BxT
|
205 |
Systematic model-based safety assessment via probabilistic model checkingGOMES, Adriano José Oliveira 31 January 2010 (has links)
Made available in DSpace on 2014-06-12T15:59:55Z (GMT). No. of bitstreams: 2
arquivo5803_1.pdf: 2496332 bytes, checksum: b4666e127bf620dbcb7437f9d83c2344 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2010 / Faculdade de Amparo à Ciência e Tecnologia do Estado de Pernambuco / A análise da segurança (Safety Assessment) é um processo bem conhecido que serve para
garantir que as restrições de segurança de um sistema crítico sejam cumpridas. Dentro dele, a
análise de segurança quantitativa lida com essas restrições em um contexto numérico
(probabilístico).
Os métodos de análise de segurança, como a tradicional Fault Tree Analysis (FTA), são
utilizados no processo de avaliação da segurança quantitativo, seguindo as diretrizes de
certificação (por exemplo, a ARP4761 Guia de Práticas Recomendadas da Aviação). No
entanto, este método é geralmente custoso e requer muito tempo e esforço para validar um
sistema como um todo, uma vez que para uma aeronave chegam a ser construídas, em média,
10.000 árvores de falha e também porque dependem fortemente das habilidades humanas para
lidar com suas limitações temporais que restringem o âmbito e o nível de detalhe que a análise e
os resultados podem alcançar. Por outro lado, as autoridades certificadoras também permitem a
utilização da análise de Markov, que, embora seus modelos sejam mais poderosos que as
árvores de falha, a indústria raramente adota esta análise porque seus modelos são mais
complexos e difíceis de lidar. Diante disto, FTA tem sido amplamente utilizada neste processo,
principalmente porque é conceitualmente mais simples e fácil de entender.
À medida que a complexidade e o time-to-market dos sistemas aumentam, o interesse em
abordar as questões de segurança durante as fases iniciais do projeto, ao invés de nas fases
intermediárias/finais, tornou comum a adoção de projetos, ferramentas e técnicas baseados em
modelos. Simulink é o exemplo padrão atualmente utilizado na indústria aeronáutica.
Entretanto, mesmo neste cenário, as soluções atuais seguem o que os engenheiros já utilizavam
anteriormente. Por outro lado, métodos formais que são linguagens, ferramentas e métodos
baseados em lógica e matemática discreta e não seguem as abordagens da engenharia
tradicional, podem proporcionar soluções inovadoras de baixo custo para engenheiros.
Esta dissertação define uma estratégia para a avaliação quantitativa de segurança baseada na
análise de Markov. Porém, em vez de lidar com modelos de Markov diretamente, usamos a
linguagem formal Prism (uma especificação em Prism é semanticamente interpretada como um
modelo de Markov). Além disto, esta especificação em Prism é extraída de forma sistemática a
partir de um modelo de alto nível (diagramas Simulink anotados com lógicas de falha do
sistema), através da aplicação de regras de tradução. A verificação sob o aspecto quantitativo
dos requisitos de segurança do sistema é realizada utilizando o verificador de modelos de Prism,
no qual os requisitos de segurança tornam-se fórmulas probabilísticas em lógica temporal.
O objetivo imediato do nosso trabalho é evitar o esforço de se criar várias árvores de falhas
até ser constatado que um requisito de segurança foi violado. Prism não constrói árvores de
falha para chegar neste resultado. Ele simplesmente verifica de uma só vez se um requisito de
segurança é satisfeito ou não no modelo inteiro.
Finalmente, nossa estratégia é ilustrada com um sistema simples (um projeto-piloto), mas
representativo, projetado pela Embraer
|
206 |
Verificação de programas C++ baseados no framework crossplataforma QtGarcia, Mário Angel Praia 13 September 2016 (has links)
Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:31Z
No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:47Z (GMT) No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:48:08Z (GMT) No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Made available in DSpace on 2017-02-07T17:48:08Z (GMT). No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5)
Previous issue date: 2016-09-13 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The software development for embedded systems is getting faster and faster, which
generally incurs an increase in the associated complexity. As a consequence, consumer electronics
companies usually invest a lot of resources in fast and automatic verification mechanisms,
in order to create robust systems and reduce product recall rates. In addition, further
development-time reduction and system robustness can be achieved through cross-platform
frameworks, such as Qt, which favor the reliable port of software stacks to different devices.
Based on that, the present work proposes a simplified version of the Qt framework, which is
integrated into a checker based on satisfiability modulo theories (SMT), name as the efficient
SMT-based bounded model checker (ESBMC++), for verifying actual Qt-based applications,
and presents a success rate of 89%, for the developed benchmark suite. We also evaluate our
simplified version of the Qt framework using other state-of-the-art verifiers for C++ programs
and an evaluation about their level of compliance. It is worth mentioning that the proposed
methodology is the first one to formally verify Qt-based applications, which has the potential to
devise new directions for software verification of portable code. / O desenvolvimento de software para sistemas embarcados tem crescido rapidamente, o
que na maioria das vezes acarreta em um aumento da complexidade associada a esse tipo de
projeto. Como consequência, as empresas de eletrônica de consumo costumam investir recursos
em mecanismos de verificação rápida e automática, com o intuito de desenvolver sistemas
robustos e assim reduzir as taxas de recall de produtos. Além disso, a redução no tempo de
desenvolvimento e na robustez dos sistemas desenvolvidos podem ser alcançados através de
frameworks multi-plataformas, tais como Qt, que oferece um conjunto de bibliotecas (gráficas)
confiáveis para vários dispositivos embarcados. Desta forma, este trabalho propõe uma versão
simplificada do framework Qt que integrado a um verificador baseado nas teorias do módulo
da satisfatibilidade, denominado Efficient SMT-Based Bounded Model Checker (ESBMC++),
verifica aplicações reais que ultilizam o Qt, apresentando uma taxa de sucesso de 89%, para
os benchmarks desenvolvidos. Com a versão simplificada do framework Qt proposto, também
foi feita uma avaliação ultilizando outros verificadores que se encontram no estado da arte para
verificação de programas em C++ e uma avalição a cerca de seu nível de conformidade. Dessa
maneira, a metodologia proposta se afirma como a primeira a verificar formalmente aplicações
baseadas no framework Qt, além de possuir um potencial para desenvolver novas frentes para a
verificação de código portátil.
|
207 |
Desenvolvimento de um mecanismo plug-and-play para o arranjo inteligente de sensores em sistemas aéreos não tripulados / Developing a plug and play mechanism for smart sensors array and unmanned aerial systemsRayner de Melo Pires 06 February 2014 (has links)
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
|
208 |
Verificação de sistemas de software baseada em transformações de código usando Bounded Model CheckingRocha, Herbert Oliveira 03 July 2015 (has links)
Submitted by Lúcia Brandão (lucia.elaine@live.com) on 2015-12-11T18:49:43Z
No. of bitstreams: 1
Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-19T14:41:05Z (GMT) No. of bitstreams: 1
Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-19T14:54:32Z (GMT) No. of bitstreams: 1
Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Made available in DSpace on 2016-01-19T14:54:32Z (GMT). No. of bitstreams: 1
Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5)
Previous issue date: 2015-07-03 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Oneofthemainchallenges insoftwaredevelopment istoensurethesafetyofthesoftwaresystems,
especially in critical embedded systems, such as aircraft or healthcare, where several constraints
(e.g., response time and data accuracy) must be met and measured in accordance with the user
requirements, otherwise a failure can lead to catastrophic situations. Thus, software verification
and testing techniques are essential items for the software development with quality, where such
techniques aim to confirm the user requirements, as well as, the predetermined behaviors for the
software.
In the software verification context, aiming the product quality, the formal verification technique
called model checking has been used to find subtle errors in actual projects of the software
systems. However, the use of the model checking technique presents some challenges such as
dealing with the model’s state explosion problem, integration with software testing environments
more familiar to designers, and handling counter-examples to reproduce the identified errors. In
order to deal with these problems, a possible solution is to explore the characteristics already
provided by the model checkers, e.g., verification of the safety properties and generation of
counter-examples. Exploring this set of characteristics, coupled with the use of program invariants
inference and a special kind of model checking, called Bounded Model Checking (BMC), this
thesis presents a set of methods to complement and enhance the scalability and accuracy of the
verification performed by Bounded Model Checkers. These methods adopted code transformation
techniques to explore the characteristics of Bounded Model Checkers to analyze the safety
properties and demonstrate errors in programs written inthe C programming language.
The methods presented in this thesis are: (1) The automatic generation and verification of the
test cases based on safety properties generated by a Bounded Model Checker for unit tests; (2)
Automating thecollection andmanipulation of thedatafrom thecounter-examples, todemonstrate
the main cause of the identified error; and (3) Adopting program invariants dynamically/statically
inferred from the analyzed program, to restrict the exploration of the states sets while performing
the verification by the BMC. This way, helping to improve the verification performed by a BMC,
related to assist in the verification and accuracy of results, by adoption of the program invariants.
The proposed approaches when used separately, provide additional options to the verification, and
interconnected, improving the code verification. Theexperimental results of theproposed methods
show to be efficient over public available benchmarks of C programs, finding errors not previously
found byother methods that are state-of-the-art. / Um dos principais desafios no desenvolvimento de software é garantir a funcionalidade dos
sistemas de software, especialmente em sistemas embarcados críticos, tais como aeronáutico ou
hospitalar, onde diversas restrições (por exemplo, tempo de resposta e precisão dos dados) devem
ser atendidas e mensuradas de acordo com os requisitos do usuário, caso contrário uma falha pode
conduzir a situações catastróficas. Logo, técnicas de verificação e teste de software são itens
indispensáveis para um desenvolvimento com qualidade, onde tais técnicas visam confirmar os
requisitos do usuário, bem como os comportamentos pré-estabelecidos para osoftware.
No contexto de verificação de software, visando à qualidade geral do produto, a técnica de
verificação formal model checking tem sido utilizada para descobrir erros sutis em projetos de
sistemas de software atuais. Contudo, a utilização da técnica model checking apresenta alguns
desafios, tais como, lidar com a explosão do espaço de estados do modelo, integração com outros
ambientes de testes mais familiares aos projetistas e tratamento e análise de contra-exemplos para
reprodução de erros. De modo a lidar com estes problemas, uma possível solução é explorar as
características já providas pelos model checkers, por exemplo, a verificação de propriedades de
segurança e geração de contra-exemplos. Explorando este conjunto de características, juntamente
com autilização dainferência deinvariantes eumtipo especial demodelchecking, denominado de
BoundedModelChecking (BMC),esta tese apresenta um conjunto de métodos para complementar
e aprimorar a escalabilidade e acurácia da verificação efetuada por Bounded Model Checkers.
Estes métodos utilizam técnicas de transformações de código para explorar as características de
Bounded Model Checkers, a fim de analisar propriedades de segurança e demonstrar erros em
códigos escritos na linguagem de programação C.
Os métodos apresentados nesta tese são: (1) A geração e verificação automática de casos de teste
baseado em propriedades de segurança geradas por um Bounded Model Checker para testes de
unidade; (2) Automatizar acoleta emanipulação das informações dos contra-exemplos, de modo a
demonstrar a causa principal do erro identificado; e (3) Utilização de invariantes
dinamicamente/estaticamente inferidas, a partir do programa analisado, para restringir a
exploração dos conjuntos de estados durante a execução da verificação pelo BMC. Desta forma,
ajudando no aprimoramento da verificação efetuada por um BMC, no que concerne em auxiliar a
sua verificação e na precisão dos resultados, pela utilização de invariantes de programas. As
abordagens propostas, quando utilizadas isoladamente, fornecem alternativas complementares a
verificação e, interligadas, aprimoram a verificação de código. Os resultados experimentais dos
métodos propostos demonstram ser eficientes sobre benchmarks públicos de programas em C,
encontrando defeitos não anteriormente encontrados por outros métodos que são estado-da-arte.
|
209 |
A CLP(FD)-based model checker for CTLEriksson, Marcus January 2005 (has links)
Model checking is a formal verification method where one tries to prove or disprove properties of a formal system. Typical systems one might want to prove properties within are network protocols and digital circuits. Typical properties to check for are safety (nothing bad ever happens) and liveness (something good eventually happens). This thesis describes an implementation of a sound and complete model checker for Computation Tree Logic (CTL) using Constraint Logic Programming over Finite Domains (CLP(FD)). The implementation described uses tabled resolution to remember earlier computations, is parameterised by choices of computation strategies and can with slight modification support different constraint domains. Soundness under negation is maintained through a restricted form of constructive negation. The computation process amounts to a fixpoint search, where a fixpoint is reached when no more extension operations has any effect. As results show, the choice of strategies does influence the efficiency of the computation. Soundness and completeness are of course independent of the choice of strategies. Strategies include how to choose the extension operation for the next step and whether to perform global or local rule instantiations, resulting in bottom-up or top-down computations respectively.
|
210 |
Parameterized verification of networks of many identical processesVérification paramétrée de réseaux composés d'une multitude de processus identiques / Vérification paramétrée de réseaux composés d'une multitude de processus identiquesFournier, Paulin 17 December 2015 (has links)
Ce travail s'inscrit dans le cadre de la vérification formelle de programmes. La vérification de modèle permet de s'assurer qu'une propriété est vérifiée par le modèle du système. Cette thèse étudie la vérification paramétrée de réseaux composés d'un nombre non borné de processus identiques où le nombre de processus est considéré comme un paramètre. Concernant les réseaux de protocoles probabilistes temporisés nous montrons que les problèmes de l'accessibilité et de synchronisation sont indécidables pour des topologies de communication en cliques. Cependant, en considérant des pertes et créations probabiliste de processus ces problèmes deviennent décidables. Pour ce qui est des réseaux dans lequel les messages n'atteignent qu'une sous partie des composants choisie de manière non-déterministe, nous prouvons que le problème de l'accessibilité paramétrée est décidable grâce à une réduction à un nouveau modèle de jeux à deux joueurs distribué pour lequel nous montrons que l'on peut décider de l'existence d'une stratégie gagnante en coNP. Finalement, nous considérons des stratégies locales qui permettent d'assurer que les processus effectuent leurs choix non-déterministes uniquement par rapport a leur connaissance locale du système. Sous cette hypothèse de stratégies locales, nous prouvons que les problèmes de l'accessibilité et de synchronisation paramétrées sont NP-complet. / This thesis deals with formal verification of distributed systems. Model checking is a technique for verifying that the model of a system under study fulfills a given property. This PhD investigates the parameterized verification of networks composed of many identical processes for which the number of processes is the parameter. Considering networks of probabilistic timed protocols, we show that the parameterized reachability and synchronization problems are undecidable when the communication topology is a clique. However, assuming probabilistic creation and deletion of processes, the problems become decidable. Regarding selective networks, where the messages only reach a subset of the components, we show decidability of the parameterized reachability problem thanks to reduction to a new model of distributed two-player games for which we prove decidability in coNP of the game problem. Finally, we consider local strategies that enforce all processes to resolve the non-determinism only according to their own local knowledge. Under this assumption of local strategy, we were able to show that the parameterized reachability and synchronization problems are NP-complete.
|
Page generated in 0.0299 seconds