Made available in DSpace on 2014-06-12T15:59:17Z (GMT). No. of bitstreams: 2 arquivo4988_1.pdf: 1332321 bytes, checksum: d7fe11f8136beac6845d4e2ab642bbda (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / Circus é uma linguagem de especificação e programação que combina CSP, Z, e construtores do Cálculo do Refinamento. A semântica de Circus está baseada na Unifying Theories of Programming (UTP). Neste trabalho, estendemos um subconjunto de Circus com operadores de tempo. A nova linguagem é denominada de Circus Time Action. Propomos um modelo novo do tempo que estende o modelo da UTP, adicionando variáveis de observação para registrar a passagem de tempo. O novo modelo é usado para dar a semântica formal de Circus Time Action. Propriedades algébricas do modelo original de Circus são validadas no novo modelo; propriedades novas são exploradas e validadas dentro do contexto de Circus Time Action. A vantagem de utilizar o padrão de unificação proposto pela UTP é poder comparar e relacionar diferentes modelos. Definimos uma função de abstração, L, que faz o mapeamento das observações registradas no novo modelo (com tempo) para observações no modelo original (sem tempo); uma função inversa, R, é também definida. O objetivo é estabelecer uma ligação formal entre o modelo novo com tempo e o modelo original da UTP. A função L e sua função inversa R formam uma Galois Connection. Usando a função de abstração, nós introduzimos a definição de programas insensíveis ao tempo. A função de abstração permite a exploração de algumas propriedades não temporais de um programa. Apresentamos um exemplo simples para ilustrar o uso da função de abstração na validação de propriedades que não têm tempo associado. Entretanto, sistemas de tempo real têm requisitos temporais que necessitam ser validados. Neste sentido, propomos um framework para a validação de requisitos não temporais usando os dois modelos e a relação entre eles. A estrutura do framework é baseada em um processo de particionamento. Tendo como ponto de partida o programa e sua especificação escritos em Circus Time Action, aplicamos uma função sintática que gera uma forma normal do programa e sua especificação. A forma normal consiste de duas partes: a primeira é um programa sem operadores de tempo, mas com eventos que, por convenção, representam ações temporais; a segunda é uma coleção de temporizadores (timers) usados pelo programa. A composição paralela de ambas as partes é semanticamente equivalente ao programa original. Usando apenas o componente da forma normal que não envolve tempo explicitamente, mostramos que é possível raciocinar sobre propriedades de tempo no modelo não temporal; provamos formalmente a validade deste resultado. Para ilustrar o uso do framework, utilizamos um sistema de alarme simplificado como estudo de caso. Como a validação é reduzida ao modelo sem tempo, usamos a ferramenta de Model-Checking de CSP (FDR) para realizar as provas mecanicamente. Esta é uma outra contribuição importante deste trabalho

DANTAS, Allberson Bruno de Oliveira. Certificação de componentes em uma plataforma de nuvens computacionais para serviços de computação de alto desempenho. 2017. 214 f. Tese (Doutorado em Ciência da Computação)-Universidade Federal do Ceará, Fortaleza, 2017. / Submitted by Gláucia Helena da Silveira Mota (glaucia@lia.ufc.br) on 2017-10-23T17:57:00Z No. of bitstreams: 1 2017_tese_abodantas.pdf: 3345763 bytes, checksum: 7d9c19651fdf5919fcc10ab432a72eeb (MD5) / Approved for entry into archive by Jairo Viana (jairo@ufc.br) on 2017-11-03T16:48:46Z (GMT) No. of bitstreams: 1 2017_tese_abodantas.pdf: 3345763 bytes, checksum: 7d9c19651fdf5919fcc10ab432a72eeb (MD5) / Made available in DSpace on 2017-11-03T16:48:46Z (GMT). No. of bitstreams: 1 2017_tese_abodantas.pdf: 3345763 bytes, checksum: 7d9c19651fdf5919fcc10ab432a72eeb (MD5) Previous issue date: 2017 / The development of correct and safe High Performance Computing (HPC) applications is a challenge for developers, since such applications generally use parallelism and run on heterogeneous parallel computing platforms. The Doctoral Thesis proposed in this document is aimed at presenting an architecture of a component certification mechanism for cloud computing platforms of high performance computing services. In particular, this mechanism is proposed within the context of the HPC Shelf platform, allowing the construction of certified components for functional and non-functional properties, which can be used to compose applications for expert users. Two particular certifier components are proposed using the certification mechanism introduced in this Thesis: SWC2 (Scientific Workflow Certifier Component) e C4 (Computation Component Certifier Component). SWC2 components are used to verify formal properties of workflows in HPC Shelf. In turn, C4 components are employed to verify formal properties on computation components. There are still tactical components, which expose the services of software formal verification infrastructures and can be orchestrated, by certifiers, by means of the TCOL (Tactical Component Orchestration Language) language, also proposed in this work. It is expected to contribute to the state-of-the-art in the following points: in cloud computing, by providing the first cloud infrastructure focused on software formal verification using exclusively high performance computing techniques; in component-oriented platforms, by providing nondisruptive components that can certify others in a reflexive way; enabling the creation of the so-called parallel certification systems, which are formed by the orchestration of provers to verify formal properties; in scientific workflows, by extracting the main verifiable patterns in these workflows; and in high performance computing applications, by providing a study on which software formal verification tools are able to verify their properties. / O desenvolvimento de aplicações de Computação de Alto Desempenho (CAD) corretas e seguras é um desafio para desenvolvedores, uma vez que tais aplicações geralmente utilizam paralelismo e executam em plataformas heterogêneas de computação paralela. A Tese de Doutorado proposta neste documento dispõe-se a apresentar a arquitetura de um mecanismo de certificação de componentes para plataformas de nuvens computacionais de serviços de computação de alto desempenho. Em particular, esse mecanismo é proposto no contexto da plataforma HPC Shelf, permitindo a construção de componentes certificados quanto a propriedades funcionais e não funcionais, os quais podem ser utilizados para compor aplicações para usuários especialistas. Dois componentes certificadores particulares são propostos utilizando o mecanismo de certificação introduzido na Tese: SWC2 (Scientific Workflow Certifier Component) e C4 (Computation Component Certifier Component). Componentes SWC2 são utilizados para verificar propriedades formais em workflows na HPC Shelf. Já os componentes C4 são empregados para verificar propriedades formais em componentes de computação. Existem ainda componentes táticos, que expõem serviços de infraestruturas de verificação formal de software e podem ser orquestrados, por certificadores, através da linguagem TCOL (Tactical Component Orchestration Language), também proposta nesse trabalho. Espera-se contribuir com o estado da arte nos seguintes pontos: em nuvens computacionais, fornecendo a primeira infraestrutura em nuvem voltada à verificação formal de software utilizando exclusivamente técnicas de CAD; em plataformas orientadas a componentes, provendo componentes não disruptivos que podem certificar outros de forma reflexiva; possibilitando a criação dos chamados sistemas de certificação paralela, os quais são formados por orquestrações de provadores para verificar propriedades formais; em workflows científicos, extraindo os principais padrões verificáveis desses workflows; e em aplicações de CAD, fornecendo um estudo sobre quais ferramentas de verificação formal de software se aplicam na verificação de suas propriedades.

Made available in DSpace on 2014-06-12T15:52:59Z (GMT). No. of bitstreams: 2 arquivo4837_1.pdf: 1490840 bytes, checksum: 1e2239b5952d87633b8a93c565229e3e (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2004 / A reestruturação de programas no contexto da orientação a objeto é também conhecida como refactoring e consiste em mudanças na estrutura interna de um software, sem modificar seu com portamento externo, a ¯m de melhorar sua legibilidade e torn¶a-lo mais f¶acil de passar por futuras mudan»cas. Na pr¶atica, refactoring baseia-se em compila»c~ao e testes para assegurar a preserva»c~ao do comportamento. Trabalhos como os de Opdyke e Roberts foram realizados com vistas µa formaliza»c~ao de refac- torings por meio da identi¯ca»c~ao de condi»c~oes que devem ser satisfeitas para assegurar que uma mudan»ca num programa preserva o comportamento do mesmo. As condi»c~oes, geralmente escritas na linguagem do c¶alculo de predicados, s~ao introduzidas como pr¶e e p¶os-condi»c~oes dos refactor- ings. Outras abordagens para a prova de preserva»c~ao do comportamento de refactorings usam formalismos como an¶alise conceitual e reescritura de grafos. Contudo, n~ao h¶a t¶ecnica alg¶ebrica que apresente refactorings como transforma»c~oes que preservam o comportamento, com prova deste fato. Nossa principal contribui»c~ao constitui-se na apresenta»c~ao de refactorings como transforma»c~oes de programas escritos em rool (Re¯nement object-oriented Language), uma linguagem baseada em Java, com classes, controle de visibilidade, liga»c~ao din^amica, e recurs~ao. A linguagem rool permite que raciocinemos sobre programas orientados a objetos e especi¯ca»c~oes, pois a mesma une estas constru»c~oes como no c¶alculo de re¯namentos de Morgan. A sem^antica de rool ¶e baseada em weakest preconditions. Um conjunto de leis de programa»c~ao est¶a dispon¶³vel tanto para os comandos imperativos de rool quanto para construtores relacionados µa orienta»c~ao a objetos. A prova, na sem^antica de rool, de que tais leis s~ao corretas, ¶e tamb¶em uma contribui»c~ao do presente trabalho. Apresentamos refactorings como regras alg¶ebricas de re¯namento envolvendo programas. A prova da preserva»c~ao do comportamento ¶e realizada pela aplica»c~ao de leis de programa»c~ao a um lado da regra a ¯m de obtermos o lado oposto. N¶os generalizamos a t¶ecnica padr~ao de re¯namento de dados a ¯m de lidar com hierarquia de classes. Neste trabalho tamb¶em apresentamos como obter um sistema estruturado segundo um padr~ao de projeto, por meio da aplica»c~ao de regras de refactoring. Padr~oes de projeto constituem-se num objetivo natural para a realiza»c~ao de transforma»c~oes por meio da aplica»c~ao de refactorings. Trabalhos presentes na literatura sobre padr~oes de projeto que prop~oem a formaliza»c~ao dos mesmos, em geral, concentram-se em suas descri»c~oes formais, n~ao na transforma»c~ao de um sistema com vistas a estrutur¶a-lo de acordo com padr~oes de projeto. Tamb¶em apresentamos a transforma»c~ao de uma aplica»c~ao monol¶³tica para uma aplica»c~ao estruturada segundo um padr~ao arquitetural.

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

Made available in DSpace on 2014-06-12T15:59:39Z (GMT). No. of bitstreams: 2 arquivo5428_1.pdf: 1146136 bytes, checksum: 397adc67935622083166ac6104064af6 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / A busca constante pelo desenvolvimento de sistemas de software com qualidade vem despertando o interesse das grandes empresas na aplicação de técnicas formais. Dentre as linguagens formais, existem aquelas próprias para a modelagem de dados complexos, tal como Z, e outras próprias para a modelagem de comunicação e concorrência, tal como CSP. Circus é uma linguagem de especificação, projeto e programação que combina Z e CSP. Além de possibilitar a especificação de aspectos de dados e comportamentais de sistema concorrentes, Circus inclui um cálculo de refinamentos. Este é seu diferencial em relação a outras integrações de Z com uma álgebra de processos. Circus vem despertando interesse no meio industrial, manifestado através de colaboraçõoes científicas e tecnológicas, e possui uma equipe envolvida na construção de ferramentas que visam facilitar sua utilização. Muitas destas ferramentas precisam de um verificador de tipos para prover mais garantias quanto a consistência das especificações e programas, e, consequentemente, de seus resultados. Neste trabalho, apresentamos uma definição formal para o sistema de tipos de Circus, com o intuito de auxiliar o desenvolvimento de um verificador de tipos para a linguagem. Optamos por primeiramente definir as regras de tipos de Circus para depois implementar o software que automatiza a aplicação dessas regras. Esta decisão de projeto contribuiu para a construção robusta do verificador, pois a implementação consiste em um mapeamento direto das regras de tipos para linhas de código. O verificador desenvolvido também oferece recursos adicionais, tais como, a disponibilidade de informações de tipos para cada fragmento da especificação ou programa passado para análise, e o fornecimento de mensagens claras e objetivas dos possíveis erros de tipos detectados ao longo da verificação. Adicionalmente, projetamos o verificador como um componente de fácil integração, manutenção e extensão. Também apresentamos neste trabalho a nossa estratégia de validação do verificador. Elaboramos testes de pequeno e grande porte, a partir de estudos de casos de sistemas reais, tal como o sistema de SmartCard que descrevemos neste trabalho. Adicionalmente, integramos o verificador com outra ferramenta: o JCircus, que é um tradutor de Circus para Java. Também implementamos uma versão inicial de uma ferramenta de refinamentos, chamada CircusRefine, para integrar o verificador de tipos. Apesar de não termos construído uma versão completa de CircusRefine, nos preocupamos em definir a arquitetura da ferramenta de tal forma que sejam possíveis futuras evoluções de forma simples e estruturada. Os testes e integrações contribuíram para a correção de defeitos da implementação e para a evolução e verificação de consistência do verificador de tipos de Circus. Ao definir o sistema de tipos de Circus, e disponibilizar um verificador de tipos, acreditamos que estamos dando uma importante contribuição na evolução de Circus, esclarecendo pontos essenciais de sua definição como uma linguagem fortemente tipada e compatível com Z e CSP, e estamos também contribuindo para o desenvolvimento de outras ferramentas da linguagem.Esperamos que o nosso trabalho possa servir de base para a definição e implementação dos sistemas de tipos das extensões de Circus

Made available in DSpace on 2014-06-12T15:59:45Z (GMT). No. of bitstreams: 2 arquivo5533_1.pdf: 1386556 bytes, checksum: dd140b25c88f8bcdd90de267c9e23d34 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / O processo de avaliação de desempenho pode ser implementado através de diversos métodos: medição que é processo de coleta de informações de um sistema real; simulação computacional e modelos analíticos que capturam o comportamento temporal de um sistema através de uma representação matemática. A avaliação baseada em modelos possibilita a análise de desempenho de sistemas, antes mesmo de sua implementação, o que possibilita ajustes ainda na fase de desenvolvimento. O uso de modelos como mecanismo de avaliação também torna possível a avaliação de cenários complexos, possibilitando, portanto, a análise de desempenho em função de restrições temporais e de recursos. O interesse na avaliação de desempenho do sistema do middleware está aumentando. O CORBA é um padrão de middleware orientado a objetos definido pela OMG que permite aplicações distribuídas em uma rede (local ou mesmo na Internet) se comuniquem. O serviço de controle de concorrência (SCC) faz parte do conjunto de serviços conhecidos como serviços comuns do CORBA e são usados por várias aplicações de diversos domínios. O SCC do CORBA foi definido para coordenar o acesso a recursos compartilhados, através do uso de locks, garantindo a consistência quando o recurso é acessado concorrentemente. Este trabalho propõe modelos redes de Petri estocástica para avaliar o desempenho do SCC do CORBA. Com a finalidade de validar os modelos propostos, os resultados da avaliação das redes de Petri são comparados com as medidas obtidas no OpenORB (núcleo do CORBA). Também são apresentados cenários de desempenho que auxiliam a tomada de decisões para melhoria do desempenho do SCC do CORBA

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.

Dissertação (mestrado)—Universidade de Brasília, Institudo de Ciências Exatas, Departamento de Ciência da Computação, 2014. / Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2014-10-21T13:01:44Z No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Approved for entry into archive by Tania Milca Carvalho Malheiros(tania@bce.unb.br) on 2014-10-22T15:32:03Z (GMT) No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Made available in DSpace on 2014-10-22T15:32:03Z (GMT). No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Uma abordagem é apresentada para verificar formalmente a corretude lógica de operadores algébricos implementados em hardware. O processo de verificação é colocado em paralelo ao fluxo convencional de projeto de hardware, permitindo a verificação de fragmentos da implementação do hardware tanto simultaneamente quanto após todo o processo de implementação ser concluído, evitando assim atrasos no projeto do circuito. A ideia principal para atestar a corretude de uma implementação em hardware é comparar seu comportamento operacional com uma definição formal de seu operador, analisando assim sua equivalência funcional; isto é, se ambas definições, de hardware e matemática, produzem os mesmos resultados quando fornecidas as mesmas entradas. A formalização dessa comparação é um desafio desta abordagem, já que as provas utilizadas para verificar a corretude e outras propriedades desses sistemas pode seguir esquemas indutivos, que proveem de maneira natural quando se trata com definições recursivas, usadas em linguagens de especificação e ferramentas de formalização. Já que Linguagens de Descrição de Hardware descrevem circuitos/sistemas de maneira imperativa, a abordagem se baseia na tradução conservativa de comandos iterativos presentes nessas linguagens em suas respectivas especificações recursivas. Esses esquemas de provas indutivas são baseados em garantir pré e pós-condições, bem como a preservação de invariantes durante todos os passos da execução recursiva, de acordo com a abordagem da lógica de Floyd-Hoare para verificação de procedimentos imperativos. A aplicabilidade da metodologia é ilustrada com um caso de estudo utilizando o assistente de prova de ordem superior PVS para fornecer prova de correção lógica de uma implementação em FPGA do algoritmo para inversão de matrizes de Gauss-Jordan (GJ). Essas provas em PVS são dadas em um estilo dedutivo baseado no Cálculo de Gentzen, aproveitando facilidades desse assistente, como tipos dependentes, indução na estrutura de tipos de dados abstratos e, é claro, suas linguagens de especificação e prova em lógica de ordem superior. ________________________________________________________________________________ ABSTRACT / An approach is introduced to formally verify the logical correctness of hardware implementations of algebraic operators. The formal verification process is placed sidelong the usual hardware design flow, allowing verification on fragments of the hardware implementation either simultaneously or after the whole implementation process finished, avoiding in this way hardware development delays. The main idea to state the correctness of a hardware implementation, is to compare its operational behavior with a formal definition of the operator, analysing their functional equivalence; that is, if both the hardware and the mathematical definition produce the same results when provided with the same entries. The formalization of this comparison is a challenge for this approach, since the proofs used to verify soundness and other properties of these systems might follow inductive schemata, that arise in a natural manner when dealing with recursive definitions, used in specifications languages of formalization tools. Since Hardware Description Languages describe circuits/systems in an imperative style, the approach is based on a conservative translation of iterative commands into their corresponding recursive specifications. The inductive proof schemata are then based on guaranteeing pre and post-conditions as well as the preservation of invariants during all steps of the recursive execution according to the Floyd-Hoare’s logical approach for verification of imperative procedures. The applicability of the methodology is illustrated with a case study using the higher-order proof assistant PVS by proving the logical correction of an FPGA implementation of the Gauss-Jordan matrix inversion algorithm (GJ). These PVS proofs are given in a Gentzen based deductive style taking advantage of nice features of this proof assistant such as dependent types and induction in the structure of abstract data types, and, of course, of its higher-order specification and proof languages.

Made available in DSpace on 2014-06-12T16:01:17Z (GMT). No. of bitstreams: 2 arquivo7289_1.pdf: 2013918 bytes, checksum: e3f26e432c831b7c299664b62269fd01 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2005 / Petróleo Brasileiro S.A. / Como outros métodos visuais orientados a objetos, UML tem influenciado tremendamente a prática de modelagem na engenharia de software com ricos mecanismos de estruturação. Porém, apesar de suas vantagens e adoção em larga escala, na prática, a falta de uma semântica formal tem dificultado o desenvolvimento rigoroso baseado em modelos de aplicações não triviais (aplicações que por sua natureza necessitam de ênfase na especificação e na verificação de seus componentes). A razão para isto é que transformações de modelos podem não preservar a semântica e, como conseqüência, o comportamento do modelo. Este problema é ainda mais sério em transformações que envolvem diferentes visões do modelo. Limitações similares podem ser encontradas durante o desenvolvimento com UML-RT. Esta linguagem é uma extensão conservativa de UML que provê a noção de objetos ativos (objetos com um comportamento próprio, independente do fluxo de execução do restante do sistema) para descrever aplicações concorrentes e distribuídas. Neste tipo de desenvolvimento, transformações devem lidar simultaneamente com as diferentes visões estáticas e dinâmicas do modelo, representadas por seus diagramas e propriedades. Por estes motivos, este trabalho propõe uma semântica para UML-RT, mapeando suas construções em OhCircus, uma linguagem formal, orientada a objetos, que combina CSP e Z, e que suporta o cálculo de refinamentos de Morgan. A partir desta semântica, bem como das noções e leis de refinamentos de OhCircus, é possível propor leis de transformação de modelos passíveis de demonstração e que preservam o comportamento do sistema. Estas leis de transformação são propostas em duas categorias: a primeira delas é um conjunto abrangente de leis básicas que expressam pequenas mudanças nas principais visões do modelo, como a declaração ou remoção de elementos do modelo; já a segunda representa leis de transformação de maior granularidade, derivadas a partir da composição de leis básicas, como a decomposição de uma cápsulas em cápsulas operando em paralelo. Tais transformações derivadas podem ser vistas como refatoramentos (refactorings) corretos sobre o modelo, facilmente aplicáveis durante um processo de desenvolvimento rigoroso, sem que o desenvolvedor tenha conhecimento do formalismo que o suporta. Finalmente, a abrangência deste conjunto de leis é discutida particularmente através dos principais passos de uma estratégia de redução de modelos UML-RT a um modelo UML estendido com um único objeto ativo, responsável por todas as interações com o ambiente e por conservar o comportamento dinâmico do sistema modelado. Este modelo UML estendido pode ser visto como uma forma normal, e, portanto, nossa estratégia pode ser vista como uma contribuição para uma estratégia mais global de completude capturada por redução a esta forma normal

Submitted by Diogo Barreiros (diogo.barreiros@ufba.br) on 2017-02-17T16:37:53Z No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-21T11:53:04Z (GMT) No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / Made available in DSpace on 2017-02-21T11:53:04Z (GMT). No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / O termo IEEE 802.11 diz respeito a uma família de especificações que buscam obter conectividade sem fio para estações fixas, portáveis e móveis em uma rede local. Redes IEEE 802.11 têm, recentemente, despertado interesse como tecnologia de suporte para a comunicação em aplicações sem fio na automação, em particular em aplicações de chão de fábrica e de controle de plantas, onde, muitas vezes, requisitos de tempo-real e requisitos de confiabilidade são necessários. Neste contexto, o uso de métodos formais permite a obtenção de um conhecimento mais preciso sobre as propriedades do protocolo bem como a especificação e verificação destas propriedades. Este trabalho apresenta uma especificação e verificação formal da função de controle de acesso ao meio da sub-camada MAC do padrão IEEE 802.11 usando UPPAAL, um verificador de modelos gratuito, que suporta os conceitos de relógios e tempo. O uso do UPPAAL permitiu considerar, dentro da modelagem, as características temporais do protocolo. A verificação procurou identificar uma série de propriedades que fornecesse aos projetistas de aplicações e sistemas de tempo-real um conjunto mínimo de garantias relativas aos canais de comunicação. Entre as propriedades verificadas, destacamos a habilidade das estações possuírem acesso ao meio dentro de um tempo finito e conhecido e, portanto, a adequação do protocolo como suporte a aplicações que necessitem de garantias temporais.