Made available in DSpace on 2014-06-12T16:00:02Z (GMT). No. of bitstreams: 2 arquivo5819_1.pdf: 1022780 bytes, checksum: 817e10825cb544dad97eed36627fdd51 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Uma abordagem formal e crucial na especificação e desenvolvimento de sistemas complexos. Inspirado pela engenharia, o desenvolvimento de software deve preterir a abordagem empirica e seguir uma abordagem estruturada, formal, passível de repetição e prova face ao advento de sistemas mais complexos, paralelos e concorrentes. Este trabalho apresenta uma extensão conservativa de OhCircus, uma linguagem de especificação oncorrente, que integra CSP, Z, orientação a objetos e um calculo de re- finamento. Esta extensão suporta a definição de heranca de processo, onde uxo de controle, operações e componentes de estado em um superprocesso, podem ser reusados por seus subprocessos. Neste trabalho nos apresentamos a gramatica estendida de OhCir- cus, acompanhada por um conjunto de regras de tipos que lidam com as novas construções da linguagem. Nos apresentamos, em termos da Unifying Theories of Programming definida por Hoare e He, a semântica formal de heranca de processo e suas construções de suporte. A principal contribuição deste trabalho e um conjunto, formalmente provado, de leis algebricas que lidam com herança de processo. Nós também explanamos informalmente como essas leis podem contribuir para uma teoria de completude para OhCircus. Finalmente nossas leis são exercitadas atraves de um estudo de caso

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