Search

O desenvolvimento de arquiteturas de controle para veículos submarinos é uma tarefa complexa. Estas podem ser caracterizadas pelos seguintes atributos: tempo real, multitarefa, concorrência e comunicações distribuídas em rede. Neste cenário, existem múltiplos processos sendo executados em paralelo, possivelmente distribuídos, e se comunicando uns com os outros. Neste contexto, o modelo comportamental pode levar a fenômenos como deadlocks, livelocks, disputa por recursos, entre outros. A fim de se tentar minimizar os efeitos de tais dificuldades, neste trabalho será apresentado um método para checagem de modelos de arquiteturas de controle de veículos submarinos baseado em Especificações Formais. A linguagem de especificação formal escolhida foi CSP-OZ, uma combinação de CSP e Object-Z. Object-Z é uma extensão orientada a objetos da linguagem Z para a especificação de predicados, tipicamente pré e pós condições, além de invariantes de dados. CSP (Communicating Sequential Process) é uma álgebra de processos desenvolvida para descrever modelos comportamentais de processos paralelos. A checagem de modelos especificados formalmente consiste na análise das especificações para verificar se um sistema possui certas propriedades através de uma busca exaustiva em todos os estados em que este pode entrar durante sua execução. Neste contexto, é possível checar corretude, livelocks, deadlocks, etc. Além disso, pode-se relacionar duas especificações diferentes a fim de se checar relações de refinamento. Para as especificações, o verificador de modelos FDR da Formal Systems Ltd. será utilizado. A implementação é desenvolvida utilizando um perfil da linguagem Ada denominado RavenSPARK, uma junção do perfil Ravenscar (desenvolvido na Universidade de York) com a linguagem SPARK (um subconjunto da linguagem Ada desenvolvido pela Praxis, Inc.). O Ravenscar é um perfil para desenvolvimento de processos, e portanto os processos de CSP, incluindo seus canais de comunicação, podem ser facilmente criados. Por outro lado, SPARK é uma linguagem onde podem ser inseridos predicados para os dados (originalmente especificados em Object-Z) utilizando anotações da própria linguagem. A linguagem SPARK possui uma ferramenta, o Examinador, que pode checar códigos de modelos baseado nestas anotações. Em resumo, o método proposto permite tanto a checagem de modelos em CSP quanto a checagem no nível de código. Para isso, as especificações em Object-Z devem inicialmente ser convertidas em um código na linguagem SPARK juntamente com suas respectivas anotações, para que então a checagem do modelo possa ser realizada no código. O desenvolvimento de uma arquitetura de controle reativa para um ROV denominado VSOR (Veículo Submarino Operado Remotamente) é utilizado como exemplo de uso do método proposto. Toda a arquitetura de controle é codificada utilizando a linguagem Ada com o perfil RavenSPARK e embarcada em um computador do tipo PC104 com o sistema operacional de tempo real VxWorks, da Windriver, Inc. The development of control architectures for Underwater Vehicles is a complex task. These control architectures might be chracterised by the following attributes: real-time, multitasking, concurrency, and distributed over communication networks. In this scenario, we have multiple processes running in parallel, possibly distributed, and engaging in communication between each other. In this context, the behavioural model might lead to phenomena like deadlocks, livelocks, race conditions, among others. In order to try to minimize the effects of such difficulties, in this work a method for model checking control architectures of underwater vehicles based on formal specifications is presented. The chosen formal specification language is CSP-OZ, a combination of CSP and Object-Z. Object-Z is an object-oriented extension of Z for the specification of predicates, typically, data pre, post and invariant conditions. CSP (Communicating Sequential Process) is a process algebra developed to describe behavioural models of parallel process. The model checking of formal specifications is a task of reasoning on specifications in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution. In this context, it is possible to check about correctness, liveness, deadlock, etc. Also, one can relate two different specifications in order to check a refinement ordering. For the specifications, the model checker FDR of Formal Systems Ltd. is utilised. The implementation is developed using an ADA language profile called RavenSPARK, a union of the Ravenscar profile (developed at the University of York) and the SPARK language (a subset of the ADA language developed by Praxis, Inc.). The Ravenscar is a profile for developing processes, so CSP processes including their message channels can be easily deployed. On the other hand, SPARK is a language where one can insert data predicates (originally specified in Object-Z) using language annotations. The SPARK language has a tool, the Examiner, that can model check code based on these annotations. In summary, the proposed method allows model checking of CSP processes but does not allow any checking in the code level. On the contrary, Object-Z specifications must first be converted into a SPARK language code, together with proper annotations, and then model checking can be realised in code. The development of a real-time reactive control architecture of an ROV named VSOR (Veiculo Submarino Operado Remotamente) is used as an example of the use of the proposed method. The whole control architecture is coded using the ADA Language with the RavenSPARK profile and deployed into a PC104 cpu system running the Vxworks real-time operating system of Windriver, Inc.

The development of network and system management software typically requires data models definition, the creation of specific applications respecting the data model, and yet the implementation of communication interfaces. Skilled professionals usually perform such tasks in a predefined sequence and using different development solutions, but any error or lacks in the data model frequently force to repeat several time-consuming tasks. In this paper we present an integrated development framework that simplifies the construction of NETCONF management applications, from data model specification to deployment and evaluation. The framework is available at http://atnog.av.it.pt/∼ptavares/ yangplugin.

O TESTE baseado em modelos visa a possibilitar a derivação de conjuntos de casos de teste a partir de especificações formais, tais como Máquinas de Estados Finitos. Os conjuntos de teste podem ser obtidos tanto pelos métodos clássicos de geração quanto por alguma abordagem ad hoc. Procura-se obter um conjunto de teste que consiga detectar todos os possíveis defeitos de uma implementação e possua tamanho reduzido para que a sua aplicação seja factível. Por questões de ordem prática, pode não ser possível a aplicação de todo o conjunto de teste gerado. Desse modo, um subconjunto de casos de teste deve ser selecionado, ou seja, uma minimização do conjunto de teste deve ser realizada. No entanto, é fundamental que a minimização reduza o custo de aplicação dos testes, mas mantenha a efetividade em revelar defeitos. Neste trabalho, propõe-se um algoritmo de minimização de conjuntos de teste para Máquinas de Estados Finitos. O algoritmo baseia-se em condições de suficiência para que a completude em relação à detecção de defeitos seja mantida. O algoritmo foi utilizado em dois diferentes contextos. Utilizou-se o algoritmo com conjuntos de teste gerados de forma aleatória para verificar a minimização obtida. O algoritmo também foi utilizado para reduzir o esforço em se obter um conjunto completo em relação à detecção de defeitos THE Model-based testing aims at generating test suites from formal specifications, such as Finite State Machines. Test suites can be obtained either from classical test derivation methods or from some ad-hoc approach. It is desirable to produce a test suite which detects all possible faults of an implementation and has small size, so that its application can be feasible. For practical reasons, the application of the generated test suite may not be possible. Therefore, a subset of test cases should be selected, i.e., a test suite minimization should be performed. However, it is important that the minimization reduces the test application cost, but keeps the effectiveness in revealing faults. In this work, an algorithm is proposed for the minimization of test suites generated from Finite State Machines. The algorithm is based on sufficient conditions, so that test suite completeness can be maintained. The algorithm was used in two different contexts. It was used with randomly generated test suites to verify the minimization obtained. The algorithm was also used to reduce the effort of obtaining a test suite with full fault coverage

Este trabalho apresenta unia nova abordagem para a avaliação de desempenho, inserindo-se nesse contexto a especificação Statecharts. Essa inserção está devidamente associada a uma solução viável para o modelo. São formalizadas duas extensões aos Statecharts: (1) os Statecharts Estocásticos, os quais utilizam a notação original dos Statecharts, modificando-se somente a semântica formal, e (2) os Queuing Statecharts, que não possuem a notação Statecharts pura, mas sim uma aglutinação entre a representação Statecharts e a de redes de filas. Na formalização proposta, são redefinidos alguns ,elementos básicos dos Statecharts, tais como eventos e condições, além de alguns conceitos da dinâmica do sistema, por exemplo, passos e configurações. As especificações propostas descrevem o funcionamento básico de um sistema de filas genérico, através de tempiates e eventos-padrão. A esses eventos estão associadas tanto uma solução analítica quanto uma solução por simulação sm p1 (iMulation Erogramming Language). Com o intuito de demonstrar a aplicabilidade das especificações propostas, é desenvolvido um estudo de caso referente à programação distribuída baseada em PVM (Para/lei Virtual Machire). Com os parâmetros obtidos empiricamente, os modelos em Statecharts Estocásticos, Queuing Statecharts e redes de Petri estocásticas generalizadas (GSPN) são alimentados e resolvidos tanto através da solução da análise do valor médio (AVM) quanto por simulação smpl. Inicialmente, a análise é feita conforme o esquema realizado pelo PVM e, posteriormente, é .acrescentado um mecanismo de escalonamento que leva em consideração o tempo médio de serviço das máquinas. Há uma discussão sobre os resultados obtidos a partir dos mecanismos adotados para realizar o escalonamento. Por fim, são expostas algumas ponderações sobre as idéias apresentadas nos capítulos componentes desta tese, além de serem apresentadas as contribuições provenientes desta pesquisa e alguns trabalhos futuros propostos a partir desta tese. This work presents a new approach to performance evaluation, introducing Statecharts in this context. That addition is associated with a viable solution for the model. Two extensions for Statecharts have been forma Iized: (1) Stochastic Statecharts, which use the original notation, with a simple modification in the formal semantics, and (2) Queuing Statecharts, which do not have the pure Statecharts notation, but a join between Statecharts and queuing network representations. In the proposed formalization, some basic elements of Statecharts are redefined, such as events and conditions, besides some concepts referring to the dynamic system behavior, e.g. steps and configurations. The proposed specifications show the basic behavior of a generic queuing isystem, by means of templates and standard events. There are solutions, both analytical methods and a smpl1 simulation, associated with each standard event. Aiming at demonstrating the applicability of the specifications proposed, a case study referring to distributed programming (based on PVM - ParalIel Virtual Machine) has been developed. Using the parameters empirically obtained, the models specified in Stochastic Statecharts, Queuing Statecharts and generalized stochastic Petri nets (GSPN) have been solved both by the Mean Value Analysis (MVA) and a smpl simulation. At the beginning, the mechanism of PVM for process scheduling is used. Afterwards, a scheduling scheme that considers the mean service time of each machine is added. A discussion about the results is carried out and some conclusions are presented. At the end, some questions about the ideas presented are exposed, along with some contributions from this thesis and some proposed future lines of research.