Concurrent software executes multiple threads or processes to achieve high performance. However, concurrency results in a huge number of different system behaviors that are difficult to test and verify. The aim of this dissertation is to develop new methods and tools for modeling and analyzing concurrent software systems at design and code levels. This dissertation consists of several related results. First, a formal model of Mondex, an electronic purse system, is built using Petri nets from user requirements, which is formally verified using model checking. Second, Petri nets models are automatically mined from the event traces generated from scientific workflows. Third, partial order models are automatically extracted from some instrumented concurrent program execution, and potential atomicity violation bugs are automatically verified based on the partial order models using model checking. Our formal specification and verification of Mondex have contributed to the world wide effort in developing a verified software repository. Our method to mine Petri net models automatically from provenance offers a new approach to build scientific workflows. Our dynamic prediction tool, named McPatom, can predict several known bugs in real world systems including one that evades several other existing tools. McPatom is efficient and scalable as it takes advantage of the nature of atomicity violations and considers only a pair of threads and accesses to a single shared variable at one time. However, predictive tools need to consider the tradeoffs between precision and coverage. Based on McPatom, this dissertation presents two methods for improving the coverage and precision of atomicity violation predictions: 1) a post-prediction analysis method to increase coverage while ensuring precision; 2) a follow-up replaying method to further increase coverage. Both methods are implemented in a completely automatic tool.

Orientador: Edmundo Roberto Mauro Madeira / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-26T19:17:39Z (GMT). No. of bitstreams: 1 Senna_CarlosRoberto_D.pdf: 8854585 bytes, checksum: 5b62fa70896f9c7e8772752a133e9514 (MD5) Previous issue date: 2014 / Resumo: Ao longo dos últimos anos bons resultados foram alcançados em iniciativas de computação paralela e distribuída que culminaram nas nuvens computacionais, transformando a Internet em uma usina virtual de processamento. Aplicações complexas organizadas através de workflows em geral são candidatas à paralelização e podem ter seu desempenho fortemente beneficiado quando executadas em grades, nuvens ou ambientes híbridos. No entanto, ainda cabe ao usuário uma parte significativa da preparação desse ambiente (software e hardware) antes de efetivamente usar todo esse poder computacional na execução de workflows. Esta tese apresenta uma infraestrutura para gerenciamento da execução de workflows de serviços fortemente acoplados em ambientes híbridos compostos por grades e nuvens computacionais. A infraestrutura denominada Cloud Execution Orchestration (CEO) é composta por um middleware que faz a gerência da execução de workflows e por uma linguagem (CEO Language - CEOL) especialmente desenhada para a construção de workflows de serviços para esses ambientes. A infraestrutura proposta suporta a execução de workflows interagindo com os domínios do ambiente (grades e nuvens) de forma transparente sem qualquer intervenção do usuário. Com a CEOL o usuário pode construir workflows abstratos, sem a localização dos recursos computacionais, pois os recursos serão escolhidos em conjunto com o escalonador e serão devidamente preparados pelo CEO para a execução. Além das funcionalidades para aprovisionamento de serviços sob demanda durante a execução de workflows, a macro arquitetura facilita a conexão da nuvem privada com nuvens públicas e oferece suporte ao processamento paralelo na medida em que opera em ambientes totalmente híbridos formados pela combinação de grades e nuvens computacionais / Abstract: Over the last few years good results have been achieved in initiatives of parallel and distributed computing that culminated in computational clouds, transforming the Internet into a virtual processing plant. Complex applications organized by workflows in general are candidates for parallelization, and can have their performance strongly benefited when executed on grids, clouds, or hybrid environments. However, it is still up to the user a significant part of preparing this environment (software and hardware) before using all that computing power for execution of workflows. This thesis presents an infrastructure for managing the execution of workflows with tightly coupled services in hybrid environments composed of grids and computational clouds. The Infrastructure, called Cloud Execution Orchestration (CEO), consists of a middleware that makes the management and execution of workflows through the CEO Language (CEOL) specially designed for building workflows of services for these environments. The proposed infrastructure supports the execution of workflows interacting with the domains of the environment (grids and clouds) transparently without any user intervention. With CEOL the user can build abstract workflows, without the location of computational resources, since resources will be chosen in conjunction with the scheduler and the CEO going to prepare them before the execution. Besides of functionalities for provisioning services on demand during the execution of workflows, the macro architecture facilitates the connection of private cloud with public cloud and supports parallel processing because may operate in hybrid environments formed by the combination of computational grids and clouds / Doutorado / Ciência da Computação / Doutor em Ciência da Computação

A Biologia Computacional tem desenvolvido algoritmos aplicados a problemas relevantes da Biologia. Um desses problemas é a Protein Structure Prediction (PSP). Vários métodos têm sido desenvolvidos na literatura para lidar com esse problema. Porém a reprodução de resultados e a comparação dos mesmos não têm sido uma tarefa fácil. Nesse sentido, o Critical Assessment of protein Structure Prediction (CASP), busca entre seus objetivos, realizar tais comparações. Além disso, os sistemas desenvolvidos para esse problema em geral não possuem interface amigável, não favorecendo o uso por não especialistas da computação. Buscando reduzir essas dificuldades, este trabalho propões o Koala, um sistema baseado em uma plataforma web, que integra vários métodos de predição e análises de estruturas de proteínas, possibilitando a execução de experimentos complexos com o uso de fluxos de trabalhos. Os métodos de predição disponíveis podem ser integrados para a realização de análises dos resultados, usando as métricas RMSD, GDT-TS ou TM-Score. Além disso, o método Sort by front dominance (baseado no critério de optimalidade de Pareto), proposto nesse trabalho, consegue avaliar predições sem uma estrutura de referência. Os resultados obtidos, usando proteínas alvo de artigos recentes e do CASP11, indicam que o Koala tem capacidade de realizar um conjunto relativamente grande de experimentos estruturados, beneficiando a determinação de melhores estruturas de proteínas, bem como o desenvolvimento de novas abordagens para predição e análise por meio de fluxos de trabalho. / Computational Biology has developed algorithms applied to relevant problems from Biology. One of these probems is Protein Structure Prediction (PSP). Several methods have been developed on the liteture to deal with this problem. However, the reproduction of results and the comparison of the methods have not been an easy task. Accordingly, the Critical Assessment of protein Structure Prediction (CASP), has among his objectives, perform these comparisons. Besides, the developed systems for this problem have low usability, not benefiting the investigation of various methods by non experts. In order to minimize those difficulties, this project proposes Koala, a web-based system that integrates several algorithms applied to PSP and analysis, allowing the execution of complex experiments by using workflows. The prediction methods can be integrated to perform some analysis of the results, by using the RMSD, GDT-TS and TM-Score metrics. Moreover, the Sort by front dominance method (based on the criterion of Pareto optimalidad), proposed on this work, can evaluate predictions with no reference structure. The results obtained, using target proteins from recent articles and CASP11, indicate that Koala has the capability to execute a relatively large set of organized experiments, benefiting determining of better protein structures, as well as the development of new approaches for prediction and analysis through workflows.

Las organizaciones que brindan servicios informáticos para el desarrollo de proyectos de investigación académica no están utilizando Enterprise Content Management (ECM), a pesar de la complejidad de la administración de documentos asociados a esta actividad. ECM permite para almacenar, entregar y gestionar contenido de forma más ágil y así poder brindar mejor servicio. En este trabajo se propone un modelo de gestión documental donde se presentan las fases que permiten implementar esta tecnología y con ello ganar capacidades nuevas en la organización. Para validar el modelo se implementó una herramienta en 2 empresas virtuales analizando los tiempos de respuesta a las solicitudes de servicio que se producían antes y después de la implementación. Además, se hizo una encuesta utilizando la escala de Likert para medirá la satisfacción de los stakeholders. / Organizations that provide computer services for the development of academic research projects are not using Enterprise Content Management (ECM), despite the complexity of document management associated with this activity. ECM allows to store, deliver and manage content more agile and thus be able to provide better service. In this paper, a document management model is proposed where the phases that allow implementing this technology are presented and thereby gain new capabilities in the organization. To validate the model, a tool was implemented in 2 virtual companies analyzing the response times to service requests that occurred before and after implementation. In addition, a survey was made using the Likert scale to measure stakeholder satisfaction. / Tesis

<p>Autonomous Mobile Robots (AMR) and IoT (Internet of Things) devices have substantial potential to increase productivity in Small and Medium Enterprises (SME). However, factors such as high costs involved in setting up and maintaining AMR automation and deficit of programming expertise among factory workers render AMR automation uneconomical for SMEs. </p><p><br></p><p></p><p>Visual Programming can be used in the spatial context of the operating environment to enable closer mental models at the right level of abstraction for novice programmers. In this thesis, we develop a system for deploying a Spatially Situated Visual Language (SSVL) for programming robot-IoT workflows. To address the challenges of interoperability, scalability, and versatility of industrial machinery, we develop a novel communication protocol based on the Resource Description Framework (RDF). Our communication protocol forms the basis of a system architecture that integrates SSVL, IoT devices, and mobile robots that enables factory workers to program AMR workflows. We design, implement and validate the system and the architecture following the systems engineering approach. To evaluate the system developed in an industrial context, we deploy the system to author AMR workflows for material handling application for an SME painting factory.</p><p></p>

Master's thesis deals with the assessment of the information system of company Dynatech s.r.o. and suggesting possible changes to improve it. In the first part of the thesis are presented the theoretical starting points, which generally define information systems, workflow, methods and analyzes that are used in the work. Another part of the thesis describes the selected company and the analyzes performed at work. The final part contains suggestions for changes to improve and streamline the information system.

This thesis describes implementation of HR change management processes of company ABB in ERP system SAP. Due to highly specific requirements for applications, standard component Personnel Change Request was not used. Authorized applicants have access to applications via SAP NetWeaver Portal. Approvers decide about approval or rejection of requests in Universal Worklist component of SAP NetWeaver Portal. Requests that require processing in HR Center are processed by employees of HR Center in SAP ERP. Applications that can be accessed via SAP NetWeaver portal were programmed with useage of framework Web Dynpro for ABAP. Processes are controlled by SAP Business Workflow.

This master's thesis is focusing to create an operational CRM system in web interface of SystemBaker application in company environment – specifically for company named Mathesio s.r.o. In theoretical part there are explained concepts and technologies, which are needed to know to fully comprehend background of the developed application. Then there are introduced possible forms of developing this application, which serve for later assessment of economic benefits of this development form. In practical part there is de-scribed structure of database, use-cases and operational solution of this application and then economical assessment of benefits of this style of development.

The goal of this master's thesis is appreciation actual estate of intradepartmental administration in company Minerva Boskovice and concept unprecedented solution. Dissertation contain analyze and concept of implementation based on present available information systems.

This thesis deals with an optimalization of the Escalation process in the customer support department in the company Centrum služeb s.r.o. It contains the analysis of the current process and theoretical knowledge to propose a new solution. The proposed solution is a website based application, which automates the process and decreases the time to resolve customers requests.