Software Transactional Memory is a promising approach to concurrent program- ming, freeing programmers from error-prone concurrency control decisions that are complicated and not composable. But few such systems address consistencies of transactional objects. In this thesis, I propose a contract-based transactional programming model toward more secure transactional sofwares. In this general model, a validity contract spec- ifies both requirements and effects for transactions. Validity contracts bring nu- merous benefits including reasoning about and verifying transactional programs, detecting and resolving transactional conflicts, automating object revalidation and easing program debugging. I introduce an ownership-based framework, namely AVID, derived from the gen- eral model, using object ownership as a mechanism for specifying and reasoning validity contracts. I have specified a formal type system and implemented a pro- totype type checker to support static checking. I also have built a transactional library framework AVID, based on existing Java DSTM2 framework, for express- ing transactions and validity contracts. Experimental results on a multi-core system show that contracts add little over- heads to the original STM. I find that contract-aware contention management yields significant speedups in some cases. The results have suggested compiler- directed optimisation for tunning contract-based transactional programs. My further work will investigate the applications of transaction contracts on various aspects of TM research such as hardware support and open-nesting.

<p>Detta arbete syftar till att undersöka hur kontrakt kan utvinnas från programkod för att skapa dokumentation som andra programmerare kan använda för att förstå hur programkoden ska användas. Kontrakt i kod fungerar både som ett sätt att hitta fel och som dokumentation så om den försvinner, exempelvis vid kompilering, kan koden bli oanvändbar för andra.</p><p>I arbetet görs en implementation vilket resulterar i ett program som kan hitta kontrakt i C++-kod och skapa XML-utdata med information om kontrakten. Programmet kan skapa mer avancerad dokumentationen genom förståelse för hur kontrakt fungerar i samband med arv. En utvärdering genom experiment av programmet visar att det har potential att bli ett användbart verktyg som underlättar återanvändning och dokumentering av programkod, men den nuvarande implementationen kan bara hantera en lite del av C++ och är därför inte praktiskt användbar.</p>

Submitted by Maria Medeiros (maria.dilva1@ufcg.edu.br) on 2018-05-18T11:37:53Z No. of bitstreams: 1 NORMANDO GOMES DE CARVALHO JÚNIOR - DISSERTAÇÃO (PPGCC) 2017.pdf: 835253 bytes, checksum: 37804bf340b68162490c02e52c346fe8 (MD5) / Made available in DSpace on 2018-05-18T11:37:53Z (GMT). No. of bitstreams: 1 NORMANDO GOMES DE CARVALHO JÚNIOR - DISSERTAÇÃO (PPGCC) 2017.pdf: 835253 bytes, checksum: 37804bf340b68162490c02e52c346fe8 (MD5) Previous issue date: 2017 / CNPq / Compreender programas é difícil porque cada trecho de código atende requisitos específicos. Em alguns casos, fatores como compreender programas que foram escritos por outras pessoas, o escopo limitado das ferramentas existentes, e a falta de documentação adicionam complexidade. Sendo assim, os desenvolvedores necessitam de uma abordagem de compreensão efetiva que diminua os custos na manutenção e que reduzam os riscos de erros, caso o entendimento do programa seja incompleto. Existem abordagens sistemáticas, apoiadas por ferramentas, para compreensão que utilizam verificações estáticas (análise do código fonte) ou dinâmicas (dados sobre a execução). As abordagens dinâmicas são utilizadas por sua efetividade, pois basta executar um teste para ver o resultado, no entanto, falham por não utilizar informações de alto nível sobre o comportamento que possam ser verificadas. Todavia, estas informações podem ser capturadas ao definir contratos, como por exemplo, na metodologia Design by Contract. Contudo, não existe uma abordagem sistemática de compreensão que utilize contratos. Este trabalho, propõe um estudo para compreender programas apoiada por uma abordagem sistematizada a fim de priorizar a escrita de contratos em programas C# utilizando os princípios de Design by Contract por meio da biblioteca Code Contracts. Podendo, mesmo assim, ser utilizada em qualquer linguagem de programação que dê suporte a Design by Contract. A avaliação foi feita em ambientes de desenvolvimento de software com 12 desenvolvedores de um centro de pesquisa e desenvolvimento em ciência da computação, considerando a aplicação da abordagem a três métodos (rotinas) de um projeto open-source. Os resultados do estudo apontam indícios de melhor compreensão dos métodos usando contratos, e por outro lado, de favorecimento da própria escrita dos contratos em métodos,a princípio desconhecidos pelos desenvolvedores. / Program comprehension is generally a difficult task, since each part of code meets specific requirements. In some cases, factors - such as comprehend programs that were written by others, limited scope of existing tools, and lack of documentation - add complexity. There fore, developers need an effective program comprehension approach that reduces maintenance costs and the risk of errors whether the program comprehension is incomplete. In order to mitigate that problem, systematic approaches are used, supported by tools, to verify comprehension using static (source code analysis) or dynamic (data on execution). Dynamic approaches are used because of their effectiveness, since they simply run a test to see the result, however, they fail to use high-level behavioral information that can be verified. Still, this information can be captured while defining contracts, for example in the Design by Contract methodology. Nevertheless, for the best of our knowledge, there is no systematic approach to program comprehension that uses contracts. In this work, we propose a study to program comprehension supported by a systematized approach, in order to prioritize the writing of contracts in C# programs using the principles of Design by Contract through the Code Contracts library. It can still be used in any programming language that supports Design by Contract. We evaluated it in software development environments with 12 developers of a research and development center in computer science, considering the approach application to three methods (routines) of an open-source project. The results of our study indicate better comprehension of methods using contracts, and, on the other hand, favoring the writing of contracts in methods, initially unknown to developers.

Detta arbete syftar till att undersöka hur kontrakt kan utvinnas från programkod för att skapa dokumentation som andra programmerare kan använda för att förstå hur programkoden ska användas. Kontrakt i kod fungerar både som ett sätt att hitta fel och som dokumentation så om den försvinner, exempelvis vid kompilering, kan koden bli oanvändbar för andra. I arbetet görs en implementation vilket resulterar i ett program som kan hitta kontrakt i C++-kod och skapa XML-utdata med information om kontrakten. Programmet kan skapa mer avancerad dokumentationen genom förståelse för hur kontrakt fungerar i samband med arv. En utvärdering genom experiment av programmet visar att det har potential att bli ett användbart verktyg som underlättar återanvändning och dokumentering av programkod, men den nuvarande implementationen kan bara hantera en lite del av C++ och är därför inte praktiskt användbar.

Industrial-scale software is commonly very large and complex, making it difficult and time-consuming to develop. In order to manage complexity in software, developers break systems into smaller components which can be developed independently. Software contracts were first proposed several decades ago; they are used to explicitly specify the interfaces between software components to ensure that they work together correctly. Software contracts specify both the responsibility of a client using a service and of the component providing the service. The advantage of contracts is that they formalise what constitutes correct interactions between software components. In addition, they serve as documentation, as well as a basis for test cases, and help clarify correct use of inheritance. However, despite their usefulness, software contracts are still not widely used in mainstream software engineering. In this work, we aim to develop a new software contract tool which we hope will help increase the use of software contracts. We start our work by evaluating existing software contract technologies and uncover a range of inconsistencies and shortcomings. We find that there are disagreements surrounding even some of the most basic aspects of software contracts. Using the lessons learned from our analysis of existing tools, we design a new contract tool, PACT. We describe in detail the formal semantics and typing of PACT and develop a first implementation of our tool. Finally, we discuss the advantages of PACT over existing tools, including its rigorous separation of interfaces and implementations, its rich inheritance semantics, and its support for flexible and expressive definition of contracts.

Submitted by Nayara Passos (nayara.passos@ufpe.br) on 2015-03-12T12:46:58Z No. of bitstreams: 2 TESE Henrique Emanuel Rabêlo.pdf: 2393775 bytes, checksum: b74f8b8b1b46d5879b334348c3110846 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Approved for entry into archive by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-03-13T12:53:22Z (GMT) No. of bitstreams: 2 TESE Henrique Emanuel Rabêlo.pdf: 2393775 bytes, checksum: b74f8b8b1b46d5879b334348c3110846 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-13T12:53:22Z (GMT). No. of bitstreams: 2 TESE Henrique Emanuel Rabêlo.pdf: 2393775 bytes, checksum: b74f8b8b1b46d5879b334348c3110846 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2014 / Design by Contract (DbC) ´e uma t´ecnica popular para desenvolvimento de programas usando especifica¸c˜oes comportamentais. Neste contexto, pesquisadores descobriram que a implementao de DbC ´e crosscutting e, portanto, sua implementa¸c˜ao ´e melhor modularizada por meio da Programa¸c˜ao Orientada a Aspectos (POA) por´em, os mecanismos de POA para dar suporte a modularide de contratos, de fato comprometem sua modularidade e entendidmento. Por exemplo, na linguagem POA AspectJ, o racioc´ınio da corretude de uma chamada de m´etodo requer uma an´alise global do programa para determinar quais advice aplicam e sobretudo o que esses advice fazem em rela¸c˜ao a implementa ¸c˜ao e checagem DbC. Al´em disso, quando os contratos so separados das classes o programador corre o risco de quebrar-los inadvertidamente. Diferentemente de uma linguagem POA como AspectJ, uma linguagem DbC preserva as principais caractersticas DbC como raciocnio modular e documenta¸c˜ao. No entanto, pr´e- e p´os-condi¸c˜oes recorrentes continuam espalhadas por todo o sistema. Infelizmente esse n˜ao o ´unico problema relacionado com modularidade que temos em linguagens DbC existentes, o seu com respectivos verificadores dinˆamicos so inconsistentes com as regras de information hiding devido a naturaze overly-dynamic na qual os contratos s˜ao checados no lado servidor. Este problema implica que durante a reportagem de erros, detalhes de implementa¸c˜ao so expostos para clientes no privilegiados. Portanto, se os programadores cuidadosamente escolherem as partes que devem ser escondidas dos clientes, durante a checagem dinˆamica de contratos, as mudanas nessas partes n˜ao deveriam afetar nem os clientes dos m´odulos nem a reportagem de erros de contratos. Neste trabalho n´os resolvemos esses problemas com AspectJML, uma nova liguagem de especifica¸c˜ao que suporta contratos crosscutting para c´odigo Java. Al´em disso, n´os demonstramos como AspectJML usa as principais caractersticas de uma linguagem DbC como racioc´ınio modular e documenta¸c˜ao dos contratos. Mais ainda, n´os mostramos como AspectJML combinado com nossa t´ecnica chamada de client-aware checking permite uma checagem dinˆamica de contratos que respeitem os princ´ıpios de information hiding em especifica¸c˜oes. Neste trabalho usamos JML para fins concretos, mas nossa solu¸c˜ao pode ser utilizadas para outras linguagems Java-likee suas respectivas linguagens DbC. Para concluir, n´os conduzimos uma avalia¸c˜ao da nossa modulariza¸c˜ao dos contratos crosscutting usando AspectJML, onde observamos que seu uso reduz o esforo de escrever pr´e- e p´os-condies, por´em com um pequeno overhead em tempo de compila¸c˜ao e instrumentação de código para checagem de contratos. / Design by Contract (DbC) is a popular technique for developing programs using behavioral specifications. In this context, researchers have found that the realization of DbC is crosscutting and fares better when modularized by Aspect-Oriented Programming. However, previous efforts aimed at supporting crosscutting contracts modularly actually compromised the main DbC principles. For example, in AspectJ-style, reasoning about the correctness of a method call may require a whole-program analysis to determine which advice applies and what that advice does relative to DbC implementation and checking. Also, when contracts are separated from classes a programmer may not know about them and may break them inadvertently. Unlike an AspectJ-like language, a DbC language keeps the main DbC principles such as modular reasoning and documentation. However, a recurrent pre- or postcondition specification remains scattered across several methods in many types. Unfortunately, this is not the only modularity problem we have with existing DbC languages. Such languages along with their respective runtime assertion checkers are inconsistent with information hiding rules because they check specifications in an overly-dynamic manner on the supplier side. This implies that during error reporting, hidden implementation details are exposed to non-privileged clients. Such details should not be used in a client’s correctness proof, since otherwise the proof would be invalidated when they change. Therefore, if programmers have carefully chosen to hide those parts “most likely” to change, most changes, in the hidden implementation details, do not affect either module clients nor DbC error reporting. In this work we solve these problems with AspectJML, a new specification language that supports crosscutting contracts for Java code. We also show how AspectJML supports the main DbC principles of modular reasoning and contracts as documentation. Additionally, we explain how AspectJML combined with our client-aware checking technique allows runtime checking to use the privacy information in specifications, which promotes information hiding. We use JML for concreteness, but the solution we propose can also be used for other Java-like languages and their respective DbC languages. To conclude, we conduct an evaluation to assess the crosscutting contract modularization using AspectJML, where we observe that its use reduces the overall design by contract code, including pre- and postconditions, but introduces a small overhead during compile time and can increase the resulting bytecode due to code instrumentation to check ordinary and crosscutting contracts

京都大学 / 0048 / 新制・課程博士 / 博士(情報学) / 甲第22675号 / 情博第728号 / 新制||情||125(附属図書館) / 京都大学大学院情報学研究科通信情報システム専攻 / (主査)教授 五十嵐 淳, 教授 山本 章博, 教授 湊 真一 / 学位規則第4条第1項該当 / Doctor of Informatics / Kyoto University / DFAM

The use of third-party components is helpful while writing complex software systems, but it can be difficult to debug software that interacts with third-party components. To address this problem, a mechanism for determining if one is using the component correctly would be beneficial. Reading component documentation may or may not help, depending on its clarity and precision. A formally specified contract for that component would be better, and would also allow run-time contract verification via assertions. The client of the component could enable these assertions during development and debugging, and then disable them for the final production release to increase performance. This thesis presents nContract, a tool that provides configurable run-time contract verification without requiring component recompilation or source code access. nContract allows component developers to formally specify .NET components using attributes. This contract information is retrieved from the compiled component's metadata and a subclass is generated for each formally specified type. All members of the component's interface are overridden and contract assertions are wrapped around calls to the base class. As long as the component client uses a factory to create instances of the component's types, the decision of whether or not to create assertion-checked or unchecked objects can be deferred until run-time. / Master of Science

Résumé : L’informatique diffuse est le passage du paradigme informatique vers l’informatique partout. L’émergence couvre principalement l’informatique mobile et distribuée, les réseaux de capteurs, l’interaction homme-machine et l’intelligence artificielle sous l’égide de l’informatique diffuse. Des efforts considérables ont été mis sur les recherches dans ce domaine, mais il n’existe pas de normes ou des méthodologies communément acceptées pour évaluer ces systèmes et de définir des nouvelles orientations de recherche dans le futur. Cette thèse s’attaque au problème d’évaluation des systèmes informatiques ubiquitaires. La question de recherche notamment le quoi et comment évaluer n’a pas encore été résolue. Dans l’objectif de trouver une réponse à cette question et d’élaborer un cadre général d’évaluation, nous avons procédé comme suit. Pour répondre à la première partie de la question, “Quoi évaluer”, nous avons tout d’abord classè les systèmes en se basant sur certains critères, et nous avons défini ensuite les principaux paramètres pour évaluer ces systèmes. Pour ce faire, nous avons étudié différents aspects de l’informatique diffuse et nous les avons classés en onze différents aspects d’évaluation. Pour chaque aspect, nous avons identifiè les principaux paramètres qui peuvent être caractérisés et mesurés. Cette taxonomie n’est pas assez exhaustive, mais elle reflète le schéma de classification le mieux adaptè pour des évaluations effectives. Cependant, pour que l’évaluation soit la plus complète possible, nous avons jugé nécessaire d’incorporer l’utilisateur dans le processus d’évaluation. À cet effet, nous avons proposè un modèle d’évaluation qui prend en compte les besoins de l’utilisateur, le contexte dans lequel la technologie sera utilisée, et l’environnement d’exploitation dans lequel le système va être déployé. Le modèle proposè constitue une première étape vers le développement des directives et standards d’évaluation qui peuvent être utilisés peuvent être utilisées pendant les évaluations formatives et sommatives. Une autre question complémentaire à l’évaluation des performances est la validation fonctionnelle d’un système en cours d’exécution, qui confirme que le système est conforme aux exigences fonctionnelles et ne contient pas de failles. Pour répondre à la deuxième partie de la question à savoir “comment évaluer”, nous avons adoptè les techniques formelles de vérification et de validation. Comme le champ d’application du projet est très large, nous sommes concentrés sur l’évaluation au premier stade de la conception afin de vérifier et de valider l’exactitude fonctionnelle de la conception de systèmes. Pour la preuve de concept, nous avons appliqué deux méthodes, dans la première méthode, nous avons étudié les approches de vérification automatique et nous avons choisi la technique la plus connue qu’est le “model checking” pour vérifier les exigences fonctionnelles d’un système de gestion des médicaments basé sur le contexte pour des personnes âgées dans une maison Intelligente. Cette approche est complémentaire aux tests et à l’évaluation et permet aux concepteurs de vérifier le comportement de leurs systèmes par rapport aux exigences fonctionnelles avant le développement du prototype de système. Certaines propriétés de base, telles que la disponibilité ou la vivacité, l’interblocage, la comparaison des spécifications et implémentations et l’analyse d’accessibilité, sont également vérifiées à ce stade. Dans la deuxième méthode, nous avons étudié les approches de vérification d’exécution et nous avons adoptè la technique de conception par le contrat pour modéliser et vérifier la sémantique et exigences de l’interopérabilité des services dans les environnements intelligents. L’avantage de cette approche réside dans la vérification automatique en temps réel de l’interopérabilité des services dans les environnements intelligents. // Abstract : Summary performance evaluations. The proposed model is a step towards forming standard evaluation guidelines that can be used during formative and summative evaluations. A complementary issue to performance evaluation is functional correctness of a running system, which confirms that the system fulfills its functional requirements and does not contain any flaws. To address the second part of the question that is “ how to evaluate ”, we have adopted the well-known formal verification and validation techniques. As the scope of the project is very big, the focus of this thesis is on early design stage evaluation to verify and validate the functional correctness of the systems design. For the proof-of-concept, we applied two methods: In the first method, we studied automatic verification approaches and used a well-known model checking approach to model and verify the functional requirements of a context aware medication management system for the elderly in a Smart House. This approach is complementary to testing and evaluation, it allows designers to verify their system behavior against its functional requirements before developing the system prototype. Some basic properties like the availability or liveliness, deadlock checking, matching of specification and implementation, and reachability analysis are verified. In the second method, we studied the runtime verification approaches and used design by contract technique to model and verify the semantic and pragmatic service interoperability requirements in smart environments. The analysis of this technique and results are presented. The benefit of the approach is automatic verification of services interoperability in smart environments on the fly.

Formal specifications describe the behaviour of object-oriented systems precisely, with the intent to capture all properties necessary for correctness. Relationships between objects, and in a broader sense the relationship between whole components, may not be adequately captured by specifications. One critical component of specifications having a role in relationships are invariants which define a constraint between multiple objects. If an object's invariant relies on external objects for its conditions, correct operations which abide by their specifications modifying these external objects may violate the constraint. Such an invariant defines a relationship between multiple objects which is unsound since it does not adequately describe the responsibilities which the objects in the relationship have to each other. The root cause of this correctness loophole is the failure of specifications to capture such relationships adequately as well as their correctness requirements. This thesis addresses this shortcoming in a number of ways, both for individual objects in a sequential environment, and between concurrent components which are defined as specialized object types. The proposed Colleague Technique [29] defines sound invariants between two object types using classical Design-by-Contract [35] methodologies. Additional invariant conditions introduced through the technique ensure that no correct operation may produce a post-state which does not satisfy all invariants satisfied by the pre-state. Relationships between objects, as well as their correct specification and management, are the subjects of this thesis. Those relationships between objects which can be described by invariants are made sound with the Colleague Technique, or the lightweight ownership type system that accompanies it. Behavioural correctness beyond these can be addressed with specifications in a similar manner to sequential systems without concurrency, in particular with the use of runtime assertion checking [11].