Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-15T15:01:06Z No. of bitstreams: 1 AMANDA SARAIVA BEZERRA - DISSERTAÇÃO PPGCC 2008..pdf: 5823735 bytes, checksum: 68f742006dbac9f251bc1a10ef99a69a (MD5) / Made available in DSpace on 2018-08-15T15:01:06Z (GMT). No. of bitstreams: 1 AMANDA SARAIVA BEZERRA - DISSERTAÇÃO PPGCC 2008..pdf: 5823735 bytes, checksum: 68f742006dbac9f251bc1a10ef99a69a (MD5) Previous issue date: 2008-11-28 / Capes / Verificar o comportamento de Sistemas Distribuídos é difícil. Algumas técnicas, como Model Checking, tentam garantir a corretude comportamental de um sistema analisando todos os seus caminhos de execução. Entretanto, esta técnica é limitada para a análise de sistemas consideravelmente pequenos. A técnica de Design by Contract (DbC) sugere a construção de um conjunto de asserções que devem ser verificadas em tempo de execução. Estas asserções são checagens instantâneas, podendo estas serem atendidas ou violadas. Como DbC não dá suporte à verificação de asserções temporais, cuja checagem deve ser realizadas sobre vários instantes,então construímos uma técnica que possibilita a verificação comportamental de Sistemas Distribuídos, verificando se a execução apresentada está de acordo com os requisitos comportamentais definidos para o sistema. Inicialmente é necessário definir os requisitos, que devem descrever o comportamento desejado para o sistema. Como estes requisitos devem ser checagens contínuas utilizamos a Lógica Temporal Linear (LTL) para descrever a evolução do comportamento ao longo do tempo. Usamos então LTL para definir o conjunto de propriedades comportamentais especificadas para o sistema distribuído implementado em Java. Cada propriedade comportamental deve ser verificada sobre um conjunto específico de objetos do sistema, são os chamados pontos de interesse. Este pontos têm relação direta e devem obedecer a uma determinada propriedade comportamental. Durante a execução é realizada a captura de informações dos pontos de interesse a serem analisados, esta captura é feita usando a Programação Orientada a Aspectos (POA). A linguagem AspectJ, implementação de POA, possibilita a captura de informações sem a necessidade de modificar o código fonte do sistema a ser analisado. Durante a execução do sistema é realizada a monitoração, além da captura da informação, sendo necessária uma ordenação parcial dos eventos provocados pelos processos que compõem o sistema distribuído. A ordenação é feita com base na relação de causa e efeito entre os eventos, assim usamos o conceito de Relógios Lógicos, que possibilita uma ordenação parcial dos eventos gerados durante a execução do sistema. Após a captura e organização dos eventos, é realizada a verificação comportamental apresentada pelos eventos de acordo com o conjunto de propriedades definidas para tal. Se em algum momento desta verificação alguma propriedade for violada, então dizemos que foi encontrado um comportamento inesperado ou anômalo, de acordo com o especificado. Esta violação é apresentada para o desenvolvedor ou testador do sistema, que tomará as devidas providências para localizar e corrigir a violação detectada. Como prova de conceito, implementamos a ferramenta DistributedDesignMonitor (DDM), realizando a monitoração de Sistemas Distribuídos implementados na linguagem Java. O DDM é apresentado e discutido através de experimentos realizados com a ferramenta, mostrando como fazer uso da técnica de monitoração. / Verify Distributed Systems is very hard. Some techniques, Model Checking for example, trying to grant the behavioral correctness analyzing all the execution paths for these systems. However, this technique is limited to check small systems. The Design by Contract technique (DbC) suggests makes a set of assertions that should be verified at runtime. These assertions are instant checks, which could be satisfied or violated. As DbC does not support the verification of temporal assertions, which check should be done over a lot of instant time for the execution, so we built a technique that verifies the Distributed Systems' behavior, verifying if the system execution is in accordance with the behavior requirements for it Initially is necessary the requirement definition, which should describe the desired system behavior. These requirements should be continuous checks, so we use the Linear Temporal Logic (LTL) to describe the evolution of the behavior over the time. The LTL is used to define set of behavioral properties specified for a Java Distributed System. Each behavioral property should be verified over defined objects of the system, they are the points of interest. These points should obey to the behavioral property defined for them. During the execution the information catch of each point of interest is done by the Aspect Oriented Programming (AOP). The language AspecU makes possible the capture of runtime information without intrusiveness. During the system execution starts the monitoring, being necessary a partial order of the events of the distributed system processes. The ordering is done based on the relation of cause and effect between events, so we use the Logical Clocks to do this partial order. After the capture and the organization of the events, the behavioral verification is done in accordance with the specified properties defined for this system. If some violation was detected during the system verification, so we found an inconsistent or unexpected behavior, in accordance with the specification. This violation is showed to the system developer or tester, which will correct the analyzed system. In this work we implemented the DistributedDesignMonitor (DDM) tool to prove our concept, monitoring Distributed Systems implemented in Java language. O DDM is presented and discussed using experiments, showed how use the monitoring technique

Client-side web applications have recently gone from progressive enhancements to powering large scale Single-page Applications (SPAs). Testing such applications is a tedious effort, often requiring manually constructing tests and emulating the browser, which leads to high programming effort and low performance. This thesis investigates how web applications can be designed, implemented and tested in order to make reliable applications with high test performance using Design by Contract (DbC) and automatically generated tests without significantly increasing programming effort. The results consist of a formal model for reactive programs using denotational and axiomatic semantics in order to not be tied to a specific programming language. The model is tested by implementing a sample application in Clojure and evaluating different aspects such as test coverage and test performance, in addition to mutation-based testing. Furthermore, the formal model can be used as a blueprint for developing reliable applications and serve as a formal building block for future research on web applications. Additionally, the sample application may be used as a guideline for real world development. The results show that applications implementing the formal model have generated test suites that are likely to detect programmer errors and can achieve high test coverage and performance while requiring less or equal effort when compared to other implementations and manual testing. / Klientbaserade webbapplikationer har under de senaste åren växt från mindre dynamiska förbättringar till att fullständigt driva Single-page Applikationer (SPAs). Att skriva tester för sådana applikationer är en komplex uppgift som ofta kräver emulering av webbläsare, vilket leder till mycket arbete och låg prestanda. Den här studien undersöker hur webbapplikationer kan designas och implementeras för att skapa pålitliga applikationer genom att använda Design by Contract (DbC) och automatiskt genererade tester, utan att signifikant påverka arbetsbördan för utvecklare. En formell modell för reaktiva applikationer presenteras med hjälp av denotationell och axiomatisk semantik för att inte begränsas till ett enskilt programspråk. Modellen testas genom utveckling och utvärdering av en exempelapplikation skriven i Clojure där olika aspekter såsom täckningsgrad och prestanda hos tester samt mutationsbaserad testning undersöks. I resultaten av den här studien presenteras en formell modell som kan användas som riktlinje för att bygga pålitliga webbapplikationer samt som en formell byggsten för framtida studier. Vidare så kan även exempelapplikationen användas som mall för utveckling av applikationer i industrin. Resultaten visar att applikationer som implementerar modellen har en testsvit som är trolig att upptäcka programmeringsfel samt uppnår hög täckningsgrad och prestanda, medan de kräver mindre eller liknande arbete som andra implementationer och manuellt programmerade tester.

This paper aims to introduce programming using Design by Contract (DbC) approach, its principles and implementations in different environments. The motivation for the creation of this approach is discussed in the beginning and the DbC metaphor is explained, as well as its application to programming. The description of major elements of the contract in the context of routine interface follows afterwards. The subject matter of this paper is the analysis and comparison of individual programming systems for DbC development with the help of code samples. The benefits of using this approach and its role in the modern development process are evaluated in conclusion.

[ES] Vivimos en una sociedad donde la digitalización está presente en nuestro día a día. Nos despertamos con la alarma de nuestro teléfono móvil, apuntamos nuestras reuniones en nuestro calendario digital, guardamos nuestros archivos en el almacenamiento en la nube, y entramos a las redes sociales prácticamente a diario. Cada una de estas acciones se ejecuta sobre un sistema software que asegura su correcto funcionamiento. Esta digitalización masiva ha hecho que el desarrollo de software se dispare en los últimos años. Durante el ciclo de vida de un sistema software, la etapa de mantenimiento supone un gasto de billones de dólares anuales. La razón detrás de este gasto es la aparición de bugs o errores que no fueron detectados durante la fase de producción del software, y que se traducen en un mal funcionamiento del sistema. Por este motivo, las técnicas de detección y localización de errores como el testeo, la verificación o la depuración son un factor clave para asegurar la calidad del software. Aunque son muchas las técnicas que se utilizan para la depuración, testeo y verificación de sistemas software, esta tesis se centra solo en algunas de ellas. En concreto, esta tesis presenta mejoras en la técnica de fragmentación de programas (depuración), una nueva metodología para hacer testeo de regresión (testeo) y una nueva implementación del modelo de verificación de diseño-por-contrato para el lenguaje de programación Erlang (verificación). Las mejoras propuestas para la técnica de fragmentación de programas incluyen diversas propuestas aplicables a diferentes escenarios: (i) mejoras en la representación y fragmentación de programas orientados a objetos, (ii) mejoras en la representación y fragmentación de estructuras de datos complejas (objetos, vectores, listas, tuplas, registros, etc.), (iii) un nuevo modelo de grafo basado en una representación más detallada de programas, aumentando la expresividad del grafo y generando fragmentos de código más precisos como resultado, y (iv) una nueva técnica para calcular fragmentos mínimos de un programa dado un conjunto específico de posibles valores de entrada. Por otro lado, la nueva metodología para hacer testeo de regresión se denomina testeo de punto de interés, e introduce la posibilidad de comparar automáticamente el comportamiento de un punto cualquiera del código dadas dos versiones del mismo sistema software. Por último, la tesis contiene la nueva implementación del modelo de verificación de programas diseño-por-contrato para el lenguaje de programación Erlang, donde se explican en detalle los nuevos tipos de contratos diseñados para las partes secuencial y concurrente de Erlang. Todos los análisis presentados en esta tesis han sido formalmente definidos y su corrección ha sido probada, asegurando de esta manera que los resultados tendrán el grado de fiabilidad necesario para ser aplicados a sistemas reales. Otra contribución de esta tesis es la implementación de dos herramientas de fragmentación de programas para dos lenguajes de programación diferentes (Java y Erlang), una herramienta para realizar testeo de punto de interés para el lenguaje de programación Erlang y un sistema para ejecutar verificación de diseño-por-contrato en Erlang. Es de destacar que todas las herramientas implementadas a lo largo del desarrollo de esta tesis son herramientas de código abierto y públicamente accesibles, de manera que pueden ser usadas o extendidas por cualquier investigador interesado en este area. / [CA] Vivim en una societat on la digitalització està present al nostre dia a dia. Ens alcem amb l'alarma del nostre telèfon mòbil, apuntem les nostres reunions al nostre calendari digital, guardem els nostres arxius al emmagatzematge al núvol, i entrem a las xarxes socials pràcticament a diari. Cadascuna d'aquestes accions s'executa sobre un sistema programari que assegura el seu correcte funcionament. Aquesta digitalizació massiva ha fet que el desenvolupament de programari es dispare en els últims anys. Durant el cicle de vida de un sistema programari, l'etapa de manteniment suposa una despesa de bilions de dòlars anuals. La raó darrere d'aquesta despesa és l'aparició de bugs o errors que no van ser detectats durant la fase de producció del programari, i que es traduïxen en un mal funcionament del sistema Per este motiu, les tècniques de detecció i localització d'errors com el testeig, la verificació o la depuració són un factor clau per a assegurar la qualitat del programari. Encara que són moltes les tècniques utilitzades per a la depuració, testeig i verificació de sistemes programari, esta tesi es centra només en algunes d'elles. En concret, esta tesi presenta millores en la tècnica de fragmentació de programes (depuració), una nova metodologia per a fer testeig de regressió (testeig) i una nova implementació del model de verificació de disseny-per-contracte per al llenguatge de programació Erlang (verificació). Les millores proposades per a la tècnica de fragmentació de programes inclouen diverses propostes aplicables a diferents escenaris: (i) millores en la representació i fragmentació de programes orientats a objectes, (ii) millores en la representació i fragmentació d'estructures de dades complexes (objectes, vectors, llistes, tuples, registres, etc.), (iii) un nou model de graf basat en una representació més detallada de programes, augmentant l'expressivitat del graf i generant fragments de codi més precisos com a resultat, i (iv) una nova tècnica per a calcular fragments mínims d'un programa donat un conjunt específic de possibles valors d'entrada. D'altra banda, la nova metodologia per a fer testeig de regressió es denomina testeig de punt d'interés, i introduïx la possibilitat de comparar automàticament el comportament d'un punt qualsevol del codi donades dos versions del mateix sistema programari. Finalment, la tesi conté la nova implementació del model de verificació de programes disseny-per-contracte per al llenguatge de programació Erlang, on s'expliquen en detall els nous tipus de contractes dissenyats per a les parts seqüencial i concurrent d'Erlang. Totes les anàlisis presentades en aquesta tesi han sigut formalment definides i la seua correcció ha sigut provada, assegurant d'aquesta manera que els resultats tindran el grau de fiabilitat necessari per a ser aplicats a sistemes reals. Una altra contribució d'aquesta tesi és la implementació de dos ferramentes de fragmentació de programes per a dos llenguatges de programació diferents (Java i Erlang), una ferramenta per a realitzar testeig the punt d'interés per al llenguatge de programació Erlang i un sistema per a executar verificació de disseny-per-contracte a Erlang. Cal destacar que totes les ferramentes implementades al llarg del desenvolupament d'aquesta tesi són ferramentes de codi obert i públicament accessibles, de manera que poden ser usades o esteses per qualsevol investigador interessat en el tema. / [EN] We live in a society where digitalisation is present in our everyday life. We wake up with the alarm of our mobile phone, book our meetings in our digital calendar, save all our media in the cloud storage, and spend time in social networks almost daily. Every one of these tasks is run over a software system that ensures its correct functionality. This massive digitalisation has made software development to shoot up in the last years. During the lifetime of software systems, the maintenance process entails a waste of billions of dollars every year. The cause of this waste is the occurrence of bugs or errors undetected during the software production, which result in a malfunction of the system. For this reason, error detection and localisation techniques, such as testing, verification, or debugging, are a key factor to ensure software quality. Although many different techniques are used for the debugging, testing, and verification of software systems, this thesis focus on only some of them. In particular, this thesis presents improvements in the program slicing technique (debugging field), a new approach for regression testing (testing field), and a new implementation of the design-by-contract verification model for the Erlang programming language (verification field). The improvements proposed for the program slicing technique include several enhancements applicable to different scenarios: (i) improvements in the representation and slicing of object-oriented programs, (ii) enhancements in the representation and slicing of (possibly recursive) complex data structures (objects, arrays, lists, tuples, records, etc.), (iii) a new graph model based on a fine-grained representation of programs that augments the expressivity of the graph and provides more accurate slicing results, and (iv) a new technique to compute minimal slices for a program given a set of specific program inputs. On the other side, the new approach for regression testing is called point of interest testing, and it introduces the possibility of automatically comparing the behaviour of any arbitrary point in the code given two versions of the same software system. Finally, the thesis presents a new implementation of the design-by-contract verification model for the Erlang programming language, where new types of contracts are explained in detail for both the sequential and concurrent parts of Erlang. All the analyses presented here have been formally defined and their correctness have been proved, ensuring that the results will have the reliability degree needed for real-life systems. Another contribution of this thesis is the implementation of two program slicers for two different programming languages (Java and Erlang), a tool to perform point of interest testing for the Erlang programming language, and a system to run design-by-contract verification in Erlang. It is worth mentioning that all the tools implemented in this thesis are open source and publicly available, so they can be used or extended by any interested researcher. / Pérez Rubio, S. (2023). Analysis Techniques for Software Maintenance [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/193146

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-22T19:52:23Z No. of bitstreams: 1 ANA EMÍLIA VICTOR BARBOSA - DISSERTAÇÃO PPGCC 2007..pdf: 1669761 bytes, checksum: f47054507fe9200c8d1d56d2848ae276 (MD5) / Made available in DSpace on 2018-08-22T19:52:23Z (GMT). No. of bitstreams: 1 ANA EMÍLIA VICTOR BARBOSA - DISSERTAÇÃO PPGCC 2007..pdf: 1669761 bytes, checksum: f47054507fe9200c8d1d56d2848ae276 (MD5) Previous issue date: 2007-04-20 / Capes / Neste trabalho propomos uma técnica que visa detectar violações de propriedades comportamentais automaticamente durante a execução de sistema de software concorrentes. A técnica foi inspirada na metodologia de desenvolvimento Design by Contract (DbC). DbC permite que os desenvolvedores adicionem aos programas asserções para que sejam verificadas em tempo de execução. O uso de asserções para expressar propriedades de programas concorrentes (multithreaded)eparalelos, entretanto,não ésuficiente. Nesses sistemas,muitas das propriedades comportamentais de interesse, como vivacidade e segurança, não podem ser expressas apenas com asserções. Essas propriedades requerem o uso de operadores temporais. Neste trabalho, utilizamos Lógica Linear Temporal (Linear Time Logic - LTL) para expressar o comportamento desejado. Para dar suporte a checagem do comportamento dos programas em tempo de execução, propomos uma técnica baseada em Programação Orientada a Aspectos, que permite que o programa seja continuamente monitorado (o comportamento é checado através do uso de autômatos que permite a deteção de comportamentos inesperados). Associada a cada propriedade comportamental existe um conjunto de pontos de interesse do código-fonte que devem obedece-la. Esses pontos são então monitorados durante a execução do sistema através do uso de aspectos. Entre outros benefícios, a técnica permite que o sistema de software alvo seja instrumentado de maneira não intrusiva, sem alterar o código-fonte — particulamente, nenhum código do software alvo deve ser modificado para execução da monitoração. Para validar este trabalho, desenvolvemos como prova de conceitos um protótipo que implementa a técnica e permite a monitoração de programas Java multi-threaded, chamado DesignMonitor. Essa ferramenta é apresentada e discutida através de um estudo de caso para demonstrar a aplicação da técnica / In this work we propose and develop a technique that allows to detect the violation of behavior properties of concurrent systems. The technique was inspired by the Design by Contract (DbC) programming methodology, which proposes the use of assertions and their evaluation at runtime to check programs behavior. The use of simple assertions to express properties of concurrent and parallel programs, however, is not sufficient. Many of the relevant properties of those systems,s uch as liveness and security, can not be expressed with simple assertions. Thesepropertiesrequiretheuseof temporal operators. In our work, we used Linear Time Logic (LTL) to specify the expected behavior. To support the runtime checking of the program against the expected behavior, we propose a technique, based on Aspect-Oriented Programming, that allows the program to be continuously monitored (behavior is checked against automata that allows the detection of unexpected behaviors). Each property is mapped to a set of points of interest in the target program. Those points are then monitored during the system execution through aspects. Among other benefits, the technique allows the instrumentation of the target software to be performed automatically and in a non-intrusive way — in particular, no code must be changed toturn monitoring on or off. To validate the work, we developed a proof of concept prototype tool that implements the technique and allows the monitoring of multi-threaded Java programs, called DesignMonitor. The tool was used in case study that has allowed the evaluation and the discussion of practical issues related with the technique.

This thesis proposes an Ecosystem perspective for the engineering of SoS and CPS and illustrates the impact of this perspective in three areas of contribution category First, from a conceptual and Systems Engineering perspective, a conceptual framework including the Ecosystems of System Unified Language Modeling (EoS-UML) profile, a set of Ecosystem Ensemble Diagrams, the Arms :Length Trust Model and the Cyber Physical Threat Model are provided. Second, having established this conceptual view of the ecosystem, we recognize unique role of the cryptographic credentials within it, towards enabling the ecosystem long-term value proposition and acting as a value transfer agent, implementing careful balance of properties meet stakeholder needs. Third, we propose that the ecosystem computers can be used as a distributed compute engine to run Collaborative Algorithms. To demonstrate, we define access control scheme, risk-balanced Cellular Access Control (rbCAC). The rbCAC algorithm defines access control within a cyber-physical environment in a manner which balances cost, risk, and net utility in a multi-authority setting. rbCAC is demonstrated it in an Air Travel and Border Services scenario. Other domains are also discussed included air traffic control threat prevention from drone identity attacks in protected airspaces. These contributions offer significant material for future development, ongoing credential and ecosystem design, including dynamic perimeters and continuous-time sampling, intelligent and self optimizing ecosystems, runtime collaborative platform design contracts and constraints, and analysis of APT attacks to SCADA systems using ecosystem approaches.