This thesis presents a component-based approach to proving the correctness of programs involving pointers. Unlike previous work, our component-based approach supports modular reasoning, which is essential to the scalability of systems. Specifically, we specify the behavior of a graph-marking algorithm known as the Schorr-Waite algorithm, implement it using a component that captures the behavior and performance benefits of pointers, and prove that the implementation is correct with respect to the specification. We use the Resolve language in our example, which is an integrated programming and specification language that supports modular reasoning. The behavior of the algorithm is fully specified using custom definitions, pre- and post-conditions, and a complex loop invariant. Additional operations for the Resolve pointer component are introduced that preserve the accessibility of a system. These operations are used in the implementation of the algorithm. They simplify the proof of correctness and make the code shorter. / Master of Science

This thesis tackles a series of problems related to the evolution of completesoftware systems both in terms of the underlying Genetic Programmingsystem and the application of that system. A new representation is presented that addresses some of the issues withother Genetic Program representations while keeping their advantages. Thiscombines the easy reproduction of the linear representation with the inheritablecharacteristics of the tree representation by using fixed-length blocks ofgenes representing single program statements. This means that each block ofgenes will always map to the same statement in the parent and child unless itis mutated, irrespective of changes to the surrounding blocks. This methodis compared to the variable length gene blocks used by other representationswith a clear improvement in the similarity between parent and child. Traditionally, fitness functions have either been created as a selection ofsample inputs with known outputs or as hand-crafted evaluation functions. Anew method of creating fitness evaluation functions is introduced that takesthe formal specification of the desired function as its basis. This approachensures that the fitness function is complete and concise. The fitness functionscreated from formal specifications are compared to simple input/outputpairs and the results show that the functions created from formal specificationsperform significantly better. A set of list evaluation and manipulation functions was evolved as anapplication of the new Genetic Program components. These functions havethe common feature that they all need to be 100% correct to be useful. Traditional Genetic Programming problems have mainly been optimizationor approximation problems. The list results are good but do highlight theproblem of scalability in that more complex functions lead to a dramaticincrease in the required evolution time. Finally, the evolution of graphical user interfaces is addressed. The representationfor the user interfaces is based on the new representation forprograms. In this case each gene block represents a component of the userinterface. The fitness of the interface is determined by comparing it to a seriesof constraints, which specify the layout, style and functionality requirements. A selection of web-based and desktop-based user interfaces were evolved. With these new approaches to Genetic Programming, the evolution ofcomplete software systems is now a realistic goal.

Um novo modelo para a especificação de hiperdocumentos denominado HMBS - Hyperdocument Model Based on Statecharts - é proposto. O HMBS adota como modelo formal subjacente a técnica Statecharts, cuja estrutura e semântica operacional são utilizadas para especificar a estrutura organizacional e a semântica de navegação de hiperdocumentos grandes e complexos. A definição do HMBS, bem como a semântica de navegação adotada, são apresentadas. Na definição apresenta-se como o modelo permite separar as informações referentes a estrutura organizacional e navegacional das representações físicas do hiperdocumento. Também são discutidas características do modelo que possibilitam ao autor analisar a estrutura do hiperdocumento, encorajando a especificação de hiperdocumentos estruturados. Para provar e validar a viabilidade prática do uso do HMBS num contexto real foi desenvolvido um ambiente de autoria e navegação de hiperdocumentos denominado HySCharts - Hyperdocumenf System based on Statecharts. Esse ambiente fornece facilidades de prototipação rápida e simulação interativa de hiperdocumentos. Para ilustrar como o modelo HMBS e o HySCharts podem ser utilizados no contexto de uma abordagem de projeto sistemática é utilizada como estudo de caso a especificação de um hiperdocumento que apresenta o Parque Ecológico de São Carlos / A new model for hyperdocument specification called HMBS - Hyperdocument Model Based on Statecharts - is proposed. HMBS uses the Statechart formalism as its underlying model. Statecharts structure and operational semantics are used to specify the organizational structure and the browsing semantics of large and complex hyperdocuments. The definition of HMBS is presented and its browsing semantics is described. It is shown how the model allows the separation of information related to the organizational and navigational structure from the hyperdocument\'s physical representation. Model features that allow authors to analyze the hyperdocument structure, encouraging the specification of structured hyperdocuments are also discussed. As a proof of concept and also to evaluate the feasibility of using HMBS in real-life applications a system called HySCharts - Hyperdocument System based on StateCharts - was developed. HySCharts is composed by an authoring and a browsing environments, supporting rapid prototyping and interactive simulation of hyperdocuments. A case study is presented that uses the specification of a hyperdocument introducing the Ecological Park of São Carlos to illustrate the use of HMBS and of the HySCharts environment integrated into a systematic design approach

Le développement de spécifications formelles correctes pour des systèmes et logiciels commence par l’analyse et la compréhension des besoins du client. Entre ces besoins décrits en langage naturel et leur spécification définie dans un langage formel précis, un écart existe et rend la tâche de développement de plus en plus difficile à accomplir. Nous sommes face à deux mondes distincts. Ce travail de thèse a pour objectif d’expliciter et d’établir des interactions entre ces deux mondes et de les faire évoluer en même temps. Par interaction, nous désignons les liens, les échanges et les activités se déroulant entre les différents documents. Parmi ces activités, nous présentons la validation comme un processus rigoureux qui démarre dès l’analyse des besoins et continue tout au long de l’élaboration de leur spécification formelle. Au fur et à mesure du développement, des choix sont effectués et les retours des outils de vérification et de validation permettent de détecter des lacunes aussi bien dans les besoins que dans la spécification. L’évolution des deux mondes est décrite via l’introduction d’un nouveau besoin dans un système existant et à travers l’application de patrons de développement. Ces patrons gèrent à la fois les besoins et la spécification formelle associée ; ils sont élaborés à partir de la description de la forme des besoins. Ils facilitent la tâche de développement et aident à éviter les risques d’oublis. Quel que soit le choix, des questions se posent tout au long du développement et permettent de déceler des lacunes, oublis ou ambiguïtés dans l’existant. / The development of correct formal specifications for systems and software begins with the analysis and understanding of client requirements. Between these requirements described in natural language and their specification defined in a specific formal language, a gap exists and makes the task of development more and more difficult to accomplish. We are facing two different worlds. This thesis aims to clarify and establish interactions between these two worlds and to evolve them together. By interaction, we mean all the links, exchanges and activities taking place between the different documents. Among these activities, we present the validation as a rigorous process that starts from the requirements analysis and continues throughout the development of their formal specification. As development progresses, choices are made and feedbacks from verification and validation tools can detect shortcomings in requirements as well as in the specification. The evolution of the two worlds is described via the introduction of a new requirement into an existing system and through the application of development patterns. These patterns manage both the requirements and their associated formal specifications ; they are elaborated from the description of the form of the requirements in the client document. They facilitate the task of development and help to avoid the risk of oversights. Whatever the choice, the proposed approach is guided by questions accompanying the evolution of the whole system and makes it possible to detect imperfections, omissions or ambiguities in the existing.

PROCESS algebras are a family of techniques used in formal specification and analysis of computer systems, specially when independent processes that perform and synchronize in parallel are concerned. The so-called concurrent systems. Circus is a process algebra that aggregates the expressiveness power for concurrent behaviors from CSP, along with the predicative data modelling aspects of Z. Recent publications have established a formal exhaustive symbolic testing theory for specifications modelled in Circus. Aiming to improve the feasibility of applying such tests in practical scenarios, it is convenient to look for criteria that reduces the number of test cases which, by the exhaustive nature of the approach, is often infinite. In the light of this, the work we present proposes the application of mutation testing techniques in Circus specifications, targeting the coverage of faults seeded by well-known mutation operators, along with operators designed with the particularities of the language in mind. Some contributions were produced in the pursuit of these goals, such as establishing a formal theory for mutation testing in Circus specifications and the implementation of a symbolic traces generator for the language. / ÁLGEBRAS de processos são uma família de técnicas de especificação e análise formal utilizadas em sistemas computacionais, especialmente em contextos de processos independentes, que atuam paralelamente e efetuam comunicação entre si. São os chamados sistemas concorrentes. Circus é uma álgebra de processos que agrega a capacidade de expressão de comportamentos concorrentes do CSP com a modelagem predicativa de dados da notação Z. Trabalhos recentes vêm estabelecer uma teoria para o teste simbólico exaustivo baseado em especificações modeladas em Circus. Com o objetivo de viabilizar a aplicação prática desses testes, é conveniente estudar critérios que reduzam o conjunto de casos de teste que, pela sua natureza exaustiva, torna-se frequentemente infinito. Neste sentido, o presente trabalho propõe a aplicação de técnicas de teste de mutação à partir de especificações Circus, visando a cobertura de falhas inseridas por meio de operadores de mutação já conhecidos, juntamente com operadores propostos especificamente para a linguagem. Algumas contribuições foram produzidas na busca destes objetivos, como o estabelecimento de uma teoria formal para a aplicação de teste de mutação em especificações Circus e a implementação de um gerador de rastros simbólicos para a mesma linguagem.

Teaching formal methods is notoriously difficult and is linked to motivation problems among the students; we think that formal methods need to be supported by adequate tools to get better acceptance from the students. One of the goals of the thesis is to build a practical tool to help students to deeply understand the classical programming methodology based on specifications, loop invariants, and decomposition into subproblems advocated by Dijkstra, Gries, and Hoare to name only a few famous computer scientists. Our motivation to build this tool is twofold. On the one hand, we demonstrate that existing verification tools (e.g., ESC/Java, Spark, SMV) are too complex to be used in a pedagogical context; moreover they often lack completeness, (and sometimes, even soundness). On the other hand teaching formal (i.e., rigorous) program construction with pen and paper does not motivate students at all. Thus, since students love to use tools, providing them with a tool that checks not only their programs but also their specifications and the structure of their reasoning seemed appealing to us. Obviously, building such a system is far from an easy task. It may even be thought completely unfeasible to experts in the field. Our approach is to restrict our ambition to a very simple programming language with simple types (limited to finite domains) and arrays. In this context, it is possible to specify problems and subproblems, both clearly and formally, using a specific assertion language based on mathematical logic. It appears that constraint programming over finite domains is especially convenient to check the kind of verification conditions that are needed to express the correctness of imperative programs. However, to conveniently generate the constraint problems equivalent to a given verification condition, we wish to have at hand a powerful language that allows us to interleave constraints generation, constraints solving, and to specify a distribution strategy to overcome the incompleteness of the usual consistency techniques used by finite domain constraint programming. We show in this thesis that the Oz language includes all programming mechanisms needed to reach our goals. Such a tool has been fully implemented and is intended to provide interesting feedback to students learning the programming method: it detects programming and/or reasoning errors and it provides typical counter-examples. We argue that our system is adapted to our pedagogical context and we report on experiments of using the tool with students in a third year programming course.

We are primarily concerned with interactive systems whose behaviour is highly reliant on end user activity. A framework for describing and synthesising such systems is developed. This consists of a functional description of the capabilities of a system together with a means of expressing its desired 'usability'. Previous work in this area has concentrated on capturing 'usability properties' in discrete mathematical models. We propose notations for describing systems in a 'requirements' style and a 'specification' style. The requirements style is based on a simple temporal logic and the specification style is based on Lamport's Temporal Logic of Actions (TLA) [74]. System functionality is specified as a collection of 'reactions', the temporal composition of which define the behaviour of the system. By observing and analysing interactions it is possible to determine how 'well' a user performs a given task. We argue that a 'usable' system is one that encourages users to perform their tasks efficiently (i.e. to consistently perform their tasks well) hence a system in which users perform their tasks well in a consistent manner is likely to be a usable system. The use of a given functionality linked with different user interfaces then gives a means by which interfaces (and other aspects) can be compared and suggests how they might be harnessed to bias system use so as to encourage the desired user behaviour. Normalising across different users anq different tasks moves us away from the discrete nature of reactions and hence to comfortably describe the use of a system we employ probabilistic rather than discrete mathematics. We illustrate that framework with worked examples and propose an agenda for further work.

Machine emulation allows for the simulation of a real or virtual machine, the source machine, on various host computers. A machine emulator interprets programs that are compiled for the emulated machine, but normally at a much reduced speed. Therefore, in order to increase the executions peed of such interpreted programs, a machine emulator may apply different dynamic optimization techniques. In our research we focus on emulators for real machines, i.e. existing computer architectures, and in particular on dynamic binary translation as the optimization technique. With dynamic binary translation, the machine instructions of the interpreted source program are translated in to machine instructions for the host machine during the interpretation of the program. Both, the machine emulator and its dynamic binary translator a resource and host machine specific, respectively, and are therefore traditionally hand-written. In this thesis we introduce the Walkabout/Yirr-Ma framework. Walkabout, initially developed by Sun Micro systems, allows among other things for the generation of instrumented machine emulators from a certain type of machine specification files. We extended Walkabout with our generic dynamic optimization framework ‘Yirr-Ma’ which defines an interface for the implementation of various dynamic optimizers: by instrumenting a Walkabout emulator’s instruction interpretation functions, Yirr-Ma observes and intercepts the interpretation of a source machine program, and applies dynamic optimizations to selected traces of interpreted instructions on demand. One instance of Yirr-Ma’s interface for dynamic optimizers implements our specification-driven dynamic binary translator, the major contribution of this thesis. At first we establish two things: a formal framework that describes the process of machine emulation by abstracting from real machines, and different classes of applicable dynamic optimizations. We define dynamic optimizations by a set of functions over the abstracted machine, and dynamic binary translation as one particular optimization function. Using this formalism, we then derive the upper bound for quality of dynamically translated machine instructions. Yirr-Ma’s dynamic binary translator implements the optimization functions of our formal framework by modules which are either generated from, or parameterized by, machine specification files. They thus allow for the adaptation of the dynamic binary translator to different source and host machines without hand-writing machine dependent code.

No presente trabalho serão apresentadas questões usuais em jogos diferenciais, nos quais os jogadores envolvidos têm objetivos diferentes; ou seja, enquanto um dos jogadores tenta fugir, o outro tenta pegar. Além disso, será definido um modelo de especificação para o jogo diferencial lobos e cordeiro. As Redes de Petri foram escolhidas como forma de especificação para o jogo proposto. Assim, o objetivo será estabelecer estratégias eficientes para o jogo lobos e cordeiro para que se possa realizar um estudo da complexidade das questões apresentadas para este jogo, levando-se em consideração a especificação formal apresentada para tal jogo. / In this work usual questions in differential games will be presented, in which the involved players have different objectives; that is, while one of the players tries "to run away", the other tries "to catch". Moreover, a specification for the differential game "wolves and lamb" will be defined. The Petri Nets had been chosen as specification formalism for the considered game. Thus, the objective is to establish efficient strategies for the game wolves and lamb so that we can carry out a study of the complexity of the presented questions, taking into consideration the presented formal specification for the game.

A Engenharia de Software vem, ao longo das últimas décadas, merecendo cada vez mais atenção da comunidade cientifica. A capacidade de construir software com qualidade, dentro dos prazos e orçamentos, atendendo a demanda do mercado, um dos objetivos almejados pelas pesquisas nesta área. Dentro deste contexto, os Métodos Formais e a Reutilização de Software tem sido utilizados para aumentar a qualidade e a produtividade de Software. Os métodos formais possibilitam o desenvolvimento e a verificação de software através de uma notação matemática rigorosa. Este rigor matemático permite que aspectos de consistência, completeza e exatidão possam ser avaliados sistematicamente. Para serem consistentes, fatos declarados em uma especificação não devem ser contraditos em outro lugar. A consistência é garantida matematicamente, provando que fatos iniciais podem ser formalmente traçados (usando-se regras de inferência). A reutilização de software a uma técnica de aproveitamento de informações produzidas durante desenvolvimentos de software anteriores, com o objetivo de reduzir o esforço necessário para o desenvolvimento de um novo sistema. 0 pressuposto básico da reutilização é produzir sistemas de maior qualidade e confiabilidade de forma mais produtiva. Assim, a produtividade é aumentada a medida que soluções de problemas anteriores podem ser aproveitadas para resolver novos problemas. Existe uma tendência de explorar a reutilização nas fases iniciais do desenvolvimento de software. Esta tendência se justifica pela grande importância dada a estas fases. Entretanto, os produtos das fases iniciais são fortemente relacionados com o domínio da aplicação, fazendo com que a reutilização de especificações, de modelos de requisitos ou estratégias de projeto só possa ser realizada com sucesso entre aplicações da mesma família, ou seja, aplicações que compartilhem requisitos e restrições. A noção de domínio é, pois, fundamental a reutilização nas fases iniciais. Um trabalho importante nesta área é o de Maiden, que pesquisou a analogia como um paradigma para reutilização de especificações de requisitos, e identificou 22 domínios abstratos representados por um conjunto de predicados. Este trabalho esta inserido no projeto PROSOFT, que a um ambiente de desenvolvimento de software construído no Grupo de Sistemas de Informação do CPGCC/UFRGS sob a coordenação do Prof. Dr. Daltro Jose Nunes e tem como objetivo apoiar o engenheiro de software desde a analise de requisitos ate a implementação do programa utilizando métodos formais. Ambientes de desenvolvimento de software que se propõem a ajudar o engenheiro de software não podem desprezar o potencial da reutilização, visto que esta técnica oferece condição de se produzir software com mais qualidade de forma mais produtiva Na atual fase de desenvolvimento do PROSOFT, não existe um modelo de reutilização. Se um usuário desejar construir um novo sistema, o ambiente não apresenta suporte para auxiliá-lo na localização e recuperação de especificações de requisitos já implementadas que poderiam ser adaptadas a uma nova solução. Portanto este trabalho tem como objetivo apresentar e especificar formalmente uma ferramenta de reutilização de requisitos para o ambiente PROSOFT. O modelo de reutilização de requisitos desenvolvido por Maiden, "reutilização de especificá-lo de requisitos por analogia" , foi utilizado como referência. / During the last decades Software Engeneering has caught the attention of the scientific community. The ability to develop Software with quality, in the time and cost estimated according to the marketing, is one of the desired goals in this research area. In this context, Formal Methods and Software Reuse have been used to improve Software's quality. Formal Methods enables the software development and verification through a rigorous mathematical notation. This mathematical rigidity allows the systematic assessment of aspects like consistency, completion and correction. The consistency is mathematicaly guaranteed, proving that initial facts are formaly traced (using inference rules). Software Reuse is a technique for making good use of the information produced in previous developments, with the purpose of reducing the efforts to develop new sytems . The basic goal in reusing is to produce systems with higher quality and robustness in a more efficient fashion. There is a tendency to explore the reuse in the initial phases of software development. This is justified by the great importance given to these phases. Nevertheless, the products of the initial phases are strongly related to the application domain, causing the specifications, requirements model or projects strategies reuse succeed only with applications of the same class, that is, applications sharing requirements and restrictions. The notion of domain is fundamental for reusability of software in the initial phases. An important work in this area is Maiden's doctoral thesis, which presents the research of the analogy as a paradigm of requirements specifications reusability , and the identification of 22 abstract domains represented by a predicate set. This work is part of the PROSOFT project, a software development environment built by the CPGCC/UFRGS Information Systems Group, with the purpose of supporting the software engineer, from the requirements analysis to the program implementation using formal methods. Software development environments that propose to help the software engineer cannot ignore the potential for reuse, as this technique offers conditions to produce higher quality software in a more productive way. In the PROSOFT's current development, there is no reuse model. If the user wants to build a new system, the environment does not have any support to help him/her in the identification and recovery of requirements specifications that could be adjusted to the new solution. Hence this work has the purpose of presenting and formaly specifying a requirement reuse tool for the PROSOFT environment. Maiden's requirement reuse model "Analogical Requirement Specification Reuse" was used as reference.