Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário. / Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.

Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.

Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.

Made available in DSpace on 2016-06-02T19:06:00Z (GMT). No. of bitstreams: 1 4702.pdf: 26018415 bytes, checksum: 9c97e5ddef6d5a00a930406e3383b476 (MD5) Previous issue date: 2012-09-19 / Financiadora de Estudos e Projetos / In the scenario of computational interfaces development, researches efforts aim to offer new ways of interaction that are closer to the natural way which humans interact with the real world. Amongst the diversity of interface modalities, the tabletop tangible interfaces make the link between physical objects and virtual objects, making possible to "grasp" the interface and interact with it physically, also counting on multitouch interactions. However, in the development process of this kind of interface, there is a lack of specification s model that supports, not only the physical objects interaction, but multitouch interactions as well, and that organizes and classifies the specification in a more agile manner, easier to document and implement. Thus, this work presents a new tabletop tangible user interface specification model, TTUI-SM, that classifies and organizes the interface element specification within many components. A diagramatic tool, TTUI-SMT, was developed based on this model, aiming to make the interface specification and development faster, easier and automatized. To validate the model and tool, two studycases were introduced and specified. An experiment was conducted to evaluate both model and tool, resulting in the comprovation, through questionnaires analysis, of the proposed benefits. / No cenário de desenvolvimento de interfaces computacionais, os avanços nas pesquisas buscam oferecer novas formas de interação que se aproximam da forma natural com que o homem interage com o mundo real. Dentre as diversas interfaces avançadas, as interfaces tangíveis de mesa (tabletop), promovem a ligação entre objetos físicos e objetos virtuais, possibilitando ao usuário interagir com objetos digitais por meio do ambiente físico, e também por meio de interações multitoques. Entretanto, o processo de desenvolvimento deste tipo de interface carece de um modelo de especificação que contemple, além das interações por meio de objetos, interações multitoques e que organize e classifique a especificação de uma maneira mais ágil e mais fácil de documentar e implementar. Assim, este trabalho apresenta um novo modelo de especificação de elementos de interface tangível de mesa, denominado TTUI-SM, que organiza a especificação de elementos de interface em diversos componentes. Uma ferramenta diagramática, o TTUI-SMT, baseada neste modelo de especificação, também foi desenvolvida visando agilizar, facilitar e automatizar o processo de especificação da interface e do seu desenvolvimento. Para validar o modelo e a ferramenta, dois estudos de caso foram introduzidos e especificados. Um experimento foi conduzido para avaliar o modelo e a ferramenta e, por meio de questionários, os benefícios propostos foram validados.