Technical Reports Published in 2013

  • IC-13-34 pdf bib
    Improving the Modeling and Analysis of Error Correction Techniques for Phase-Change Memory.
    Caio Hoffman, Luiz E. da S. Ramos, Rodolfo J. de Azevedo, and Guido C. S. de Araújo.
    December 2013. In English, 21 pages.

    Abstract: Due to projections of high scalability, Phase-Change Memory (PCM) is seen as a new main memory for computer systems. In fact, PCM may even replace DRAM, whose scaling limitations require new lithography technologies that are still unknown. On the down-side, PCM has low endurance when compared with DRAM, i.e., on average, a PCM cell can only withstand $10^8$ bit-flips (modification of stored bit values) before the cell fails. To address PCM's low endurance, Error Correction Techniques (ECTs) have been proposed, which aim at increasing PCM's lifetime. However, previous lifetime analyses of ECTs have not considered the difference between the bit-flip frequencies of data bits and code bits (used to correct errors in data bits). That observation is crucial for the correct analysis of the ECTs since high bit-flip frequencies lead to faster wear-out.

    In this work, we improve the wear-out analysis of PCM by modeling and analyzing the bit-flip probabilities of five ECTs, namely, ECP, DRM, SECDED, SAFER, and FREE-p. We then use our analysis to evaluate the impact of error correction on the wear-out of PCM. To do our analyses, we mathematically modeled and simulated the ECTs using both a theoretical bit-flip probability (50%) and an empirical bit-flip rate (15%), obtained from the execution of SPEC CPU2006. Our results show clear endurance degradation in techniques that use error-correcting codes, which contradicts some previous results in the literature. Finally, we analyzed the power consumption of the ECTs, and found that ECP and SAFER exhibit the best trade-off between endurance and write energy.

  • IC-13-33 pdf bib
    Partial fsm models and completeness with blocking test cases.
    Adilson Luiz Bonifacio and Arnaldo Vieira Moura.
    November 2013. In English, 15 pages.

    Abstract: Test suite generation and coverage analysis have been widely studied for FSM-based models. Several studies focused on specific conditions for verifying completeness of test suites. Some have found necessary conditions for test suite completeness, whereas other approaches obtained sufficient, but not necessary, conditions for this problem. Most of these works restricted the specification or the implementation FSM models in several ways. More recent works have described necessary and sufficient conditions for test suite completeness, but only under the assumption that all implementations be complete FSM models. In this work we describe necessary and sufficient conditions for test suite completeness under more relaxed constraints. We also show an intrinsic relation between the number of states in implementations and complete test suites. Further we show necessary and sufficient conditions for test suite completeness in the presence of blocking sequences in both the specification and the implementation models.

  • IC-13-32 pdf bib
    Trade-off Between Bandwidth and Energy Consumption Minimization in Virtual Network Mapping.
    Esteban Rodriguez, Gustavo Alkmim, Daniel Batista, and Nelson da Fonseca.
    October 2013. In English, 13 pages.

    Abstract: Network virtualization is a promising technology for the Internet of the Future. Nevertheless, an open issue in virtualization is to satisfy the control of resources in a way that energy savings are achieved. This paper introduces a model for the mapping of virtual networks onto network substrates which aims to reduce the energy consumption as well as to reduce the bandwidth consumption. This model is based on an integer linear programming formulation and several parameters, corresponding to characteristic of real networks, are considered. The trade-off between energy and bandwidth consumption is analyzed based on results derived via simulation.

  • IC-13-31 pdf bib
    Live Migration in Green Virtualized Networks.
    Esteban Rodriguez, Gustavo Alkmim, Daniel Batista, and Nelson da Fonseca.
    October 2013. In English, 12 pages.

    Abstract: Network virtualization is a promising technology for the Internet of the Future. An open issue in virtualization is the management of network resources in a way that energy savings are achieved without compromising the Quality of Service (QoS) requirements of the virtual networks. The dynamic allocation and deallocation of virtual networks can lead the state of the substrate to a less than optimum energy consumption. This paper introduces two algorithms for the migration of virtual routers and/or links which aims to allocate resources so that energy consumption is minimized. The efficacy of the migration of virtual routers and/or links and its impact on energy consumption are analyzed based on results derived via simulations.

  • IC-13-30 pdf bib
    Green Virtualized Networks.
    Esteban Rodriguez, Gustavo Alkmim, Daniel Batista, and Nelson da Fonseca.
    October 2013. In English, 14 pages.

    Abstract: The Future Internet demands energy efficient communication to cope with the ever increasing power consumption. Virtualization techniques have proved to be effective in reducing power consumption of network devices. An open issue in virtualization for green networking is the search for an energy-efficient mapping of virtual networks onto physical networks. This paper introduces a new model for the mapping of virtual networks which aims at reducing the energy consumption. This model is based on an integer linear programming formulation and several parameters, corresponding to characteristic of real networks, are considered. Simulation results attest the efficacy of the proposal.

  • IC-13-29 pdf bib
    Approximated Algorithms for Mapping Virtual Networks on Network Substrates.
    Gustavo Alkmim, Daniel Batista, and Nelson da Fonseca.
    October 2013. In English, 14 pages.

    Abstract: Network virtualization is a promising technique for building the Internet of the future since it enables the introduction of new features into network elements at low cost. An open issue in virtualization is how to search for an efficient mapping of virtual network elements onto those of the existing physical network. Mapping is an NP-hard problem and existing solutions take long time to find a solution. This paper presents four new approximated algorithms based on two integer linear programming formulations that runs fast and, also, consider various real network characteristics, which is neglected by other proposals in the literature.

  • IC-13-28 pdf bib
    Optimal Mapping of Virtual Networks.
    Gustavo Alkmim, Daniel Batista, and Nelson da Fonseca.
    October 2013. In English, 15 pages.

    Abstract: Network virtualization is a promising technique for building the Internet of the future since it enables the low cost introduction of new features into network elements. An open issue in virtualization is how to search for an efficient mapping of virtual network elements onto those of the existing physical network, also called the substrate network. Mapping is an NP-hard problem and existing solutions ignore various real network characteristics in order to solve problem in a reasonable time frame. This paper introduces two new algorithms for the solution of the mapping problem, both based on 0–1 integer programming, for the solution of the mapping problem which consider a whole new set of network parameters not taken into account by previous proposals. Simulation experiments confirm the efficiency of the proposed algorithms.

  • IC-13-27 pdf bib
    Querying complex data.
    Luiz Gomes-Jr, Luciano da F. Costa, and André Santanchè.
    October 2013. In English, 19 pages.

    Abstract: Database technology has advanced to support increasingly complex data - from relations to semi-structured data and unstructured documents. More recently, graph databases have regained attention following demands from applications like social networks and recommendation systems. Graph analysis, usually associated with the Complex Networks field, has become a central tool in areas such as biology, physics and linguistics. Database management systems should improve support to these data and applications beyond the data model level tackled by current graph databases, including more flexible querying models and management mechanisms.

    In this paper, we define the characteristics of the highly interconnected data that underlies many of these modern applications. We adopt the term complex data as a reference to the field of complex networks. A database management system for complex data requires a flexible query model that explores the topology of the relationships, taking into account their eventual uncertainty. Efficient query processing becomes a challenge, requiring new mechanisms for relationship-based query optimizations.

    To meet the new requirements, our solution models complex data as property graphs with weighted relationships. We propose a new query language that allows ranking of elements based on properties of the topology of the graph. The queries are evaluated based on a variation of the spreading activation model, which is the core of the query processor and the main target for query optimization strategies. Experiments with real data show the practicability of our approach and support our analysis of several query optimization and approximation mechanisms.

  • IC-13-26 pdf bib
    Time Hybrid Total Order Broadcast: Exploiting the Inherent Synchrony of Asynchronous Broadcast-based Distributed Systems.
    Daniel Cason and Luiz E. Buzato.
    October 2013. In English, 30 pages.

    Abstract: Informally, total order broadcast protocols allow processes to send messages with the guarantee that all processes eventually deliver the messages in the same order. In this paper, we investigate the efficiency and performance of a very simple synchronous total order broadcast protocol, that is built atop a broadcast-based asynchronous distributed system. The performance results allow us to conclude that our Time Hybrid Total Order Broadcast (THyTOB) represents an interesting trade-off between performance and simplicity for total order broadcasts; its simplicity also allows its use as a benchmark for total order broadcast atop Ethernet. Finally, the experimental results that support THyTOB make a strong case for the reconsideration of the common wisdom that total order broadcasts must be always designed for the asynchronous model because it is the best way to guarantee safety and performance.

  • IC-13-25 pdf bib
    Alternative Routing and Zone-Based Spectrum Assignment Algorithm for Flexgrid Optical Networks.
    Rafael A. Scaraficci and Nelson L. S. da Fonseca.
    October 2013. In English, 13 pages.

    Abstract: In optical flexgrid networks, the optical spectrum can be allocated at a much finer granularity that it can be allocated in fixed-grid WDM networks, and connections can use a variable number of slots. However, the dynamic establishment and tear down of lightpaths demanding variable spectrum widths yields to the fragmentation of the spectrum with increase in blocking of connections; mainly connections demanding large spectrum widths. This papers proposes a novel algorithm that introduces a zone-based assignment policy together with an alternative path routing mechanism based on the maximum capacity available. Results derived via simulation using different topologies and considering connections requests from 40Gbps to 1000Gbps, show that the proposed algorithm leads to blocking ratio consistently lower than those given by traditional approaches. Furthermore, it reduces the blocking ratio of high rates connections, in some cases, in more than six times.

  • IC-13-24 pdf bib
    Fragmentation Aware Routing and Spectrum Assignment Algorithm.
    Pedro M. Moura - Nelson L. S. da Fonseca  - Rafael A. Scaraficci.
    October 2013. In English, 11 pages.

    Resumo: In flex-grid (elastic) networks, the spectrum can be allocated at a much finer granularity than it can be allocated in WDM networks. However, the dynamic establishment and tear down of lightpaths yields to the fragmentation of the spectrum with consequent increase in blocking of requests for connection establishment. Therefore, it is of paramount importance that allocation decisions try to mitigate the fragmentation problem. In line with that, this paper introduces the Multigraph Shortest Path Algorithm for novel Routing and Spectrum Allocation (RSA) in elastic networks. Results indicate that the joint use of the new algorithm with proposed cost functions can produce bandwidth blocking ratio four orders of magnitude lower than existing RSA algorithms.

  • IC-13-23 pdf bib
    Algorithm for FIPP p-cycle Path Protection in Flexgrid Networks.
    Helder M. N. S. Oliveira - Nelson L. S. da Fonseca.
    October 2013. In English, 12 pages.

    Abstract: In optical networks, faults in links and nodes cause massive loss of data even if for short periods. Therefore, protection techniques have been developed to cope with failures. Among these techniques, p-cycle is very attractive since it provides ring-like speed of restoration in mesh topologies. In recent years, the technology of flexgrid networks has emerged as a solution for dealing with the diversity of bandwidth demands of network applications. However, very few investigations have been proposed for path protection in flexgrid networks. This paper introduces a novel algorithm to provide Failure-independent path protecting p-cycle for path protection in flexgrid networks. Results indicate that the 100% protection for single failures provided by the algorithm produces low overhead under different scenarios and provide protection for dual failures at a certain extend in networks with large connectivity.

  • IC-13-22 pdf bib
    Dominating sets in planar graphs.
    Patrícia F. Hongo and C. N. Campos.
    September 2013. In English, 18 pages.

    Abstract: A dominating set of a graph $G$ is a subset $D\subseteq V(G)$ such that each vertex of $G$ is in $D$ or is adjacent to a vertex in $D$. The cardinality of a minimum size dominating set for $G$ is denoted by $\gamma(G)$. In 1996, Tarjan and Matheson proved that $\gamma(G)\leq  n/3$ for triangulated discs and conjectured that $\gamma(G)  \leq n/4$ for triangulated planar graphs with sufficiently large $n$. In the present work, we verify the conjecture for two simple classes of triangulated planar graphs.

  • IC-13-21 pdf bib
    Necessity and sufficiency for checking m-completeness of test suites.
    Adilson Luiz Bonifacio and Arnaldo Vieira Moura.
    September 2013. In English, 15 pages.

    Abstract: Test suite generation for Finite State Machines (FSM) has been largely investigated. Some of the previous work in this area found necessary, but not sufficient, conditions for the automatic generation of test suites for this class of models. Yet other set of previous studies obtained sufficient, but not necessary, conditions for the same problem. Many earlier works imposed several conditions upon the specification or on the implementation models. Here, we describe necessary and sufficient conditions for the automatic generation of $m$-complete test suites when the specification and implementation are modeled as FSMs. Further, we impose only weak a priori restrictions on the models, such as determinism and completeness of implementation models. We do not require reduced models nor complete specifications.

  • IC-13-20 pdf bib
    Generating asymptotically non-terminant initial variable values for linear diagonalizable programs.
    Rachid Rebiha, Arnaldo V. Moura, and Nadir Matringe.
    September 2013. In English, 20 pages.

    Abstract: We present the key notion of asymptotically non-terminant initial variable values for non-terminant loop programs. We show that those specific values are directly associated to inital variable values for which the corresponding loop program does not terminate. Considering linear diagonalizable programs, we describe powerful computational methods that generate automatically and symbolically a semi-linear space represented by a linear system of equalities and inequalities. Each element of this space provides us with asymptotically non-terminant initial variable values. Our approach is based on linear algebraic methods. We obtain specific conditions using certain basis and matrix encodings related to the loop conditions and instructions.

  • IC-13-19 pdf bib
    MPSoCBench: A Benchmark Suite for Evaluating Multiprocessor System-on-Chip Tools and Methodologies.
    Liana Duenha and Rodolfo Azevedo.
    August 2013. In English, 29 pages.

    Abstract: The consolidated use of multiprocessors in the embedded systems designs introduces new important challenges for system architects and hardware/software designers. In particular, it becomes necessary to develop tools based on new paradigms, able to deal with MPSoC complexities. Recent design methodologies and tools are focused on enhancing the design productivity by providing a software development platform before the final MPSoC architecture details are fixed. However, the simulation can only be efficiently implemented when using a modeling and simulation engine that supports the system behavior description in a high abstraction level. The lack of multiprocessor platforms integrating both scalable hardware and software in order to design and evaluate new methodologies and tools motivated us to develop MPSoCBench, which is a benchmark composed by a scalable set of MPSoCs including four different ISAs (PowerPC, MIPS, SPARC, and ARM), organized in platforms with 1, 2, 4, 8, 16, 32, or 64 cores, with different interconnections (router or NoCs), capable of running 13 parallel version of software from well known parallel benchmarks. The tool also provide power consumption estimation for MIPS and SPARC processors. The benchmark sums 828 distinct configurations automated through scripts.

  • IC-13-18 pdf bib
    Colorings and crossings.
    Atílio Gomes Luiz and R. Bruce Richter.
    August 2013. In English, 32 pages.

    Abstract: In 2007, Albertson conjectured that if a graph $G$ has chromatic number $k$, then the crossing number of $G$ is at least the crossing number of the complete graph with $k$ vertices. To date, two papers were written on this subject trying to solve the conjecture for an arbitrary $k$-chromatic graph $G$, and after much effort the conjecture was proved true for $k 
         \leq  16$. In this report, we present an overview of topics related to Albertson's Conjecture, such as: the crossing number problem, lower bounds on crossing number, lower bounds on the number of edges of color-critical graphs, and coloring of graphs with small crossing number and small clique number. While investigating Albertson's conjecture, J. Barát and G. Tóth proposed the following conjecture involving color-critical graphs: for every positive integer $c$, there exists a bound $k(c)$ such that for any $k$, where $k  \geq  k(c)$, any k-critical graph on $k+c$ vertices has a subdivision of $K_k$. In Section $9$, we present counterexamples to this conjecture for every $c  \geq  6$ and we prove that the conjecture is valid for $c =
         5$.

  • IC-13-17 pdf bib
    Design principles for affectibility.
    Elaine C. S. Hayashi and M. Cecilia C. Baranauskas.
    July 2013. In English, 31 pages.

    Abstract: The design for (with and by) children in learning contexts faces challenges to bring children’s real life experiences into interactive systems, including their affective responses – which are not often considered in design processes. In the endeavor of providing practical information on the design of learning technology that is explicitly concerned with the affective responses of children, we present our investigation on Design Principles. The principles that we present here are based on empirical data and, at the same time, supported by a priori knowledge. Practical application of the principles is explored in the analysis of two existing activities for children on the educational XO laptop from OLPC.

  • IC-13-16 pdf bib
    Patterns in Environmental Event Processing.
    I. Koga and C. B. Medeiros.
    July 2013. In English, 18 pages.

    Abstract: Environmental scientists have to deal with large amounts of heterogeneous data. To accomplish their scientific goals, they have to overcome data management problems that range from the acquisition to the storage of data. This paper is concerned with solving some of the problems at the stage of data analysis. We developed a framework that enables the integration of different types of data sources and detection of relevant events considering the integrated data that flows through the framework. A key aspect of our approach is that it allows treating static and dynamic data sources homogeneously. A case study using real data from meteorological stations is discussed showing the feasibility of our framework.

  • IC-13-15 pdf bib
    Anais do VIII Workshop de Teses, Dissertações e Trabalhos de Iniciação Cientí­fica em Andamento do IC-UNICAMP.
    Alessandra Gomes - Ariadne Carvalho - Divino César - Elisa Rodrigues - Ewerton Silva - Fabio A. Faria - Fabricio Gonçalves - Flavio Nicastro - Greice Mariano - Gustavo Alkmim - Ivelize Bernardo - Ivo Koga - Juliana G. Greghi - Leonardo Tampelini - Leonardo Tizzei - Marcelo Palma - Matheus Mota - Maxiwell Garcia - Priscila T. M. Saito - Roberto Pereira - Ricardo Dutra - Rosana S. Takehara - Vanessa Maike  - Walisson Pereira.
    July 2013. Partly in English, partly in Portuguese, 60 pages.

    Resumo: Este relatório técnico contém os resumos de 10 trabalhos apresentados no VIII Workshop de Teses, Dissertações e Trabalhos de Iniciação Científica, do Instituto de Computação da Universidade Estadual de Campinas (WTD-IC-UNICAMP 2013). O Workshop ocorreu nos dias 11 e 12 de junho de 2013 e contou com aproximadamente 92 participantes, entre ouvintes, apresentadores de trabalhos e organizadores. Na ocasião houve 16 apresentações orais e 3 pôsteres. Aos alunos foi dada a possibilidade de escolher a forma de apresentação (oral, pôster, ou ambas). A publicação dos resumos, sob forma de relatório técnico, tem por objetivo divulgar os trabalhos em andamento e registrar, de forma sucinta, o estado da arte da pesquisa do IC no ano de 2013.

  • IC-13-14 pdf bib
    Conjuntos Dominantes e Produto Direto de Ciclos.
    A. R. Oliveira e C. N. Campos.
    June 2013. In Portuguese, 7 pages.

    Resumo: Este trabalho determina o idomatic number do produto direto de um ciclo com quatro vértices e um ciclo com $n$ vértices. Além disso, é determinado um limitante inferior simples para a cardinalidade do conjunto dominante independente mínimo destes grafos.

  • IC-13-13 pdf bib
    A LLVM Just-in-Time Compilation Cost Analysis.
    Rafael Auler and Edson Borin.
    May 2013. In English, 23 pages.

    Abstract: The compilation time and generated code quality are important factors of a Just-in-Time (JIT) compilation Dynamic Binary Translation (DBT) system. In order to decide which optimization level to apply, a good DBT must know in advance for how long it will halt the execution system until the optimization finishes. If this time is known, the system can make a better judgment on which subset of optimizations it should use. Nevertheless, the algorithms used for code optimization and generation execute a number of steps that is difficult to predict. The algorithms complexity in time is dependent on a transitory input that changes every time a pass from the compilation pipeline finishes. For worklist-based algorithms, the worst-case time and average-case time may differ greatly, affecting the usefulness of an analytical approach to time estimation. This technical report presents an analysis of the LLVM compilation cost and proposes a model to predict this compilation cost as a function of code properties. We use an empirical approach that provides an easy way to understand the behavior of code generation performance and provide a quantitative analysis of the compilation time of all C and C++ functions from the SPEC CPU2006 benchmarks. We also show that the error of our final model is under 21% for 90% of the tests.

  • IC-13-12 pdf bib
    Fulkerson's Conjecture and Loupekine Snarks.
    Kaio Karam and C. N. Campos.
    May 2013. In English, 14 pages.

    Abstract: In 1976, F. Loupekine created a method for constructing new snarks from already known ones. In the present work, we consider an infinite family of Loupekine's snarks constructed from the Petersen Graph, and verify Fulkerson's Conjecture for this family.

  • IC-13-11 pdf bib
    Um estudo do desempenho da multiplicação de matrizes em arquiteturas modernas.
    Caian Benedicto, Edson Borin, and Philippe Remy Bernard Devloo.
    April 2013. In Portuguese, 20 pages.

    Resumo: Nesse trabalho nós analisamos o impacto no desempenho causado por variações no algoritmo de multiplicação de matrizes densas e como esse impacto varia ao utilizarmos um compilador com estratégias diferentes de otimização. Comparamos o resultado obtido com as bibliotecas fornecidas por fabricantes de hardware para 2 sistemas distintos e também comparamos com com os resultados de desempenho obtidos utilizando-se a plataforma de programação paralela OpenCL.

  • IC-13-10 pdf bib
    On finite automata with quantum and classical states.
    Alex Bredariol Grilo and Arnaldo Vieira Moura.
    April 2013. In English, 15 pages.

    Abstract: Finite automata with quantum and classical states were proposed to study the influence of Quantum Mechanics in simpler computational devices. In this work, we study the topic focusing on computability and complexity questions. We show results presented in the literature involving languages recognizability and closure properties and we then present some partial results on languages not recognized by the model.

  • IC-13-09 pdf bib
    Tradução taxonômica: o caso do sinbiota.
    Cleber Mira, Pedro Feijão, João Meidanis, Tiago Duque-Estrada, and Carlos Joly.
    March 2013. In Portuguese, 20 pages.

    Abstract: O Sistema de Informação Ambiental (SinBiota 1.0), desenvolvido para integrar as informações sobre a biodiversidade do estado de São Paulo geradas pelo programa BIOTA/FAPESP, possui por volta de 18 mil nomes científicos adicionados por diversos pesquisadores ao longo de um período de mais de dez anos. Esses termos podem apresentar diversos tipos de problemas, como erros de digitação, ou a espécie pode ter mudado de nome oficial, tornando-se o termo um sinônimo do nome corrente. Nesse trabalho apresentamos uma estratégia de resolução desses problemas para identificar os nomes científicos válidos no SinBiota, por meio de uma tradução dos termos atualmente cadastrados com base na classificação taxonômica suportada por uma iniciativa internacional.

  • IC-13-08 pdf bib
    A complete approach for termination analysis of linear programs.
    Rachid Rebiha, Nadir Matringe, and Arnaldo V. Moura.
    February 2013. In English, 23 pages.

    Abstract: We describe powerful computational methods, relying on new decidability results that respond completely to major conjectures on termination analysis of programs with conditional linear loops, on all initial values. Our approach is based on linear algebraic methods: we reduce the verification of the termination problem to checking the orthogonality of a well determined vector-space and a certain vector, both related to the loop. We obtain necessary and sufficient conditions from which we provide the first complete method, which determines the termination of such a class of linear programs. Our examples (dealing with a large number of randomly generated linear loops) show the strength of our results, we actually prove that some of them are beyond the limits of other recent approaches.

  • IC-13-07 pdf bib
    Necessary and sufficient condition for termination of linear programs.
    Rachid Rebiha, Nadir Matringe, and Arnaldo V. Moura.
    February 2013. In English, 22 pages.

    Abstract: We describe new decidability results that respond completely to major conjectures on termination analysis of linear loop programs, on all initial values interpreted over the reals. To the best of our knowledge, we present the first necessary and sufficient conditions from which we provide a complete decidability result and methods for termination analysis of such a class of programs. We reduce the termination analsysis for such programs to the problem consisting in checking if a specific vector (related to the loop condition encoding) belong to a specific vectorial space related to the matrix encoding the assignements of the loop variables. We provide theoretical results guaranteeing the soundness and completeness of the termination analysis while restrincting the variables interpretation over a specific countable subring of the field of real numbers.

  • IC-13-06 pdf bib
    Transcendental invariants generation for non-linear hybrid systems.
    Rachid Rebiha, Arnaldo V. Moura, and Nadir Matringe.
    February 2013. In English, 26 pages.

    Abstract: We present the first verification methods that automatically generate bases of invariants expressed by multivariate formal power series and transcendental functions. We discuss the convergence of solutions generated over hybrid systems that exhibit non-linear models augmented with parameters. We reduce the invariant generation problem to linear algebraic matrix systems, from which one can provide effective methods for solving the original problem. We obtain very general sufficient conditions for the existence and the computation of formal power series invariants over multivariate polynomial continuous differential systems. The formal power series invariants generated are often composed by the expansion of some well-known transcendental functions like "log" or "exp" and have an analysable closed-form. This facilitates their use to verify safety properties. Moreover, we generate inequality and equality invariants. Our examples, dealing with non-linear continuous evolution similar to those present today in many critical hybrid embedded systems, show the strength of our results and prove that some of them are beyond the limits of other recent approaches.

  • IC-13-05 pdf bib
    Generating invariants for non-linear hybrid systems.
    Rachid Rebiha, Arnaldo V. Moura, and Nadir Matringe.
    February 2013. In English, 36 pages.

    Abstract: We describe powerful computational techniques, relying on linear algebraic methods, for generating ideals of non-linear invariants of algebraic hybrid systems. We show that the preconditions for discrete transitions and the Lie-derivatives for continuous evolution can be viewed as morphisms, and so can be suitably represented by matrices. We reduce the non-trivial invariant generation problem to the computation of the associated eigenspaces by encoding the new consecution requirements as specific morphisms represented by such matrices. More specifically, our methods are the first to establish very general sufficient conditions that show the existence and allow the computation of invariant ideals. Our methods also embody a strategy to estimate certain degree bounds, leading to the discovery of rich classes of inductive, i.e. provable, invariants. By reducing the problem to related linear algebraic manipulations we are able to address various deficiencies of other state-of-the-art invariant generation methods, including the efficient treatment of non-linear hybrid systems. Our approach avoids first-order quantifier elimination, Grobner basis computation or direct system resolution, thereby circumventing difficulties met by other recent techniques.

  • IC-13-04 pdf bib
    Generating invariants for non-linear loops by linear algebraic methods.
    Rachid Rebiha, Arnaldo V. Moura, and Nadir Matringe.
    February 2013. In English, 37 pages.

    Abstract: We present new computational methods that can automate the discovery and the strengthening of non-linear interrelationships among the variables of programs containing non-linear loops, that is, that give rise to multivariate polynomial and fractional relationships. Our methods have complexities lower than the mathematical foundations of the previous approaches, which used Grobner basis computation, quantifier elimination or cylindrical algebraic decomposition. We show that the preconditions for discrete transitions can be viewed as morphisms over a vector space of degree bounded by polynomials. These morphisms can, thus, be suitably represented by matrices. We also introduce fractional and polynomial consecution, as more general forms for approximating consecution. The new relaxed consecution conditions are also encoded as morphisms represented by matrices. By so doing, we reduce the non-linear loop invariant generation problem to the computation of eigenspaces of specific morphisms. Moreover, as one of the main results, we provide very general sufficient conditions allowing for the existence and computation of loop invariant ideals. As far as it is our knowledge, it is the first invariant generation methods that handle multivariate fractional loops. Our algorithm also incorporates a strategy to guess the degree bounds which allow for the generation of ideals of non-trivial invariants.

  • IC-13-03 pdf bib
    Statistical Multiplexing of Multifractal Flows.
    Cesar A. V. Melo and Nelson L. S. da Fonseca.
    February 2013. In English, 14 pages.

    Abstract: This paper introduces the computation of an expression for the time at which the length of a queue fed by several multifractal flows reaches its maximum. Expressions for the equivalent bandwidth of an aggregate of multifractal flows is also presented. Moreover, it is shown that modelling based on monofractal process rather than based on multifractal processes leads to overprovisioning of resources.

  • IC-13-02 pdf bib
    An Envelope Process for Multifractal Traffic Modeling.
    Cesar A. V. Melo and Nelson L. S. da Fonseca.
    February 2013. In English, 13 pages.

    Abstract: In this paper, a novel envelope process for multifractal traffic modeling is introduced. The envelope process is an upper bound for the amount of work arrived in a multifractal Brownian motion process. The time scale of interest of a queueing system fed by a multifractal stream is computed. Simulation experiments using both real and synthetic data show that the proposed model is accurate.

  • IC-13-01 pdf bib
    The Web Within: leveraging Web standards and graph analysis to enable application-level integration of institutional data.
    Luiz Gomes-Jr and André Santanchè.
    January 2013. In English, 22 pages.

    Abstract: The expansion of the Web and of our capacity of producing and storing information have had a profound impact on the way we organize, manipulate and share data. We have seen an increased specialization of database back-ends and data models to respond to modern application needs: text indexing engines organize unstructured data, standards and models were created to support the Semantic Web, BigData requirements stimulated an explosion of data representation and manipulation models. This complex and heterogeneous environment demands unified strategies that enable data integration and, especially, cross-application, expressive querying.

    Here we present a new approach for the integration of structured and unstructured data within organizations. In our framework, diverse data models are integrated in a unifying graph. A novel query model allows the combination of concepts from Information Retrieval and Database Management Systems into a declarative query language. This query language enables flexible correlation queries over the unified data that can be used to support a wide range of applications.

    We show how Web technologies such as RDF can be leveraged to integrate institutional data. In our approach, the SPARQL query language is extended to enable the new query model. We also present examples of application of the model in several areas, such as CMSs, recommendation systems, social networks, etc. Experimental results demonstrate the viability of our approach in real scenarios.


  • Instituto de Computação :: Universidade Estadual de Campinas
    Av. Albert Einstein, 1251 - Cidade Universitária Zeferino Vaz • 13083-852 Campinas, SP - Brasil • Fone: [19] 3521-5838