-
Naming the Pain in Machine Learning-Enabled Systems Engineering
Authors:
Marcos Kalinowski,
Daniel Mendez,
Görkem Giray,
Antonio Pedro Santos Alves,
Kelly Azevedo,
Tatiana Escovedo,
Hugo Villamizar,
Helio Lopes,
Teresa Baldassarre,
Stefan Wagner,
Stefan Biffl,
Jürgen Musil,
Michael Felderer,
Niklas Lavesson,
Tony Gorschek
Abstract:
Context: Machine learning (ML)-enabled systems are being increasingly adopted by companies aiming to enhance their products and operational processes. Objective: This paper aims to deliver a comprehensive overview of the current status quo of engineering ML-enabled systems and lay the foundation to steer practically relevant and problem-driven academic research. Method: We conducted an internation…
▽ More
Context: Machine learning (ML)-enabled systems are being increasingly adopted by companies aiming to enhance their products and operational processes. Objective: This paper aims to deliver a comprehensive overview of the current status quo of engineering ML-enabled systems and lay the foundation to steer practically relevant and problem-driven academic research. Method: We conducted an international survey to collect insights from practitioners on the current practices and problems in engineering ML-enabled systems. We received 188 complete responses from 25 countries. We conducted quantitative statistical analyses on contemporary practices using bootstrap** with confidence intervals and qualitative analyses on the reported problems using open and axial coding procedures. Results: Our survey results reinforce and extend existing empirical evidence on engineering ML-enabled systems, providing additional insights into typical ML-enabled systems project contexts, the perceived relevance and complexity of ML life cycle phases, and current practices related to problem understanding, model deployment, and model monitoring. Furthermore, the qualitative analysis provides a detailed map of the problems practitioners face within each ML life cycle phase and the problems causing overall project failure. Conclusions: The results contribute to a better understanding of the status quo and problems in practical environments. We advocate for the further adaptation and dissemination of software engineering practices to enhance the engineering of ML-enabled systems.
△ Less
Submitted 20 May, 2024;
originally announced June 2024.
-
Experimental comparison of 5G SDR platforms: srsRAN x OpenAirInterface
Authors:
Ruan P. Alves,
Joao Guilherme A. da S. Alves,
Mikael R. Camelo,
Wilker O. de Feitosa,
Victor F. Monteiro,
Fco. Rodrigo P. Cavalcanti
Abstract:
A Software-Defined Radio (SDR) platform is a communication system that implements as software functions that are typically implemented in dedicated hardware. One of its main advantages is the flexibility to test and deploy radio communication networks in a fast and cheap way. In the context of the Fifth Generation (5G) of wireless cellular networks, there are open source SDR platforms available on…
▽ More
A Software-Defined Radio (SDR) platform is a communication system that implements as software functions that are typically implemented in dedicated hardware. One of its main advantages is the flexibility to test and deploy radio communication networks in a fast and cheap way. In the context of the Fifth Generation (5G) of wireless cellular networks, there are open source SDR platforms available online. Two of the most popular SDR platforms are srsRAN and OpenAirInterface. This paper presents these two platforms, the characteristics of the networks created by them, the possibilities of changes in their interfaces and configurations, and also their limits. Moreover, in this paper, we also evaluate and compare both platforms in an experimental setup deployed in a laboratory.
△ Less
Submitted 3 June, 2024;
originally announced June 2024.
-
Offline robot programming assisted by task demonstration: an AutomationML interoperable solution for glass adhesive application and welding
Authors:
M. Babcinschi,
F. Cruz,
N. Duarte,
S. Santos,
S. Alves,
P. Neto
Abstract:
Robots have been successfully deployed in both traditional and novel manufacturing processes. However, they are still difficult to program by non-experts, which limits their accessibility to a wider range of potential users. Programming robots requires expertise in both robotics and the specific manufacturing process in which they are applied. Robot programs created offline often lack parameters t…
▽ More
Robots have been successfully deployed in both traditional and novel manufacturing processes. However, they are still difficult to program by non-experts, which limits their accessibility to a wider range of potential users. Programming robots requires expertise in both robotics and the specific manufacturing process in which they are applied. Robot programs created offline often lack parameters that represent relevant manufacturing skills when executing a specific task. These skills encompass aspects like robot orientation and velocity. This paper introduces an intuitive robot programming system designed to capture manufacturing skills from task demonstrations performed by skilled workers. Demonstration data, including orientations and velocities of the working paths, are acquired using a magnetic tracking system fixed to the tools used by the worker. Positional data are extracted from CAD/CAM. Robot path poses are transformed into Cartesian space and validated in simulation, subsequently leading to the generation of robot programs. PathML, an AutomationML-based syntax, integrates robot and manufacturing data across the heterogeneous elements and stages of the manufacturing systems considered. Experiments conducted on the glass adhesive application and welding processes showcased the intuitive nature of the system, with path errors falling within the functional tolerance range.
△ Less
Submitted 21 May, 2024;
originally announced May 2024.
-
ML-Enabled Systems Model Deployment and Monitoring: Status Quo and Problems
Authors:
Eduardo Zimelewicz,
Marcos Kalinowski,
Daniel Mendez,
Görkem Giray,
Antonio Pedro Santos Alves,
Niklas Lavesson,
Kelly Azevedo,
Hugo Villamizar,
Tatiana Escovedo,
Helio Lopes,
Stefan Biffl,
Juergen Musil,
Michael Felderer,
Stefan Wagner,
Teresa Baldassarre,
Tony Gorschek
Abstract:
[Context] Systems incorporating Machine Learning (ML) models, often called ML-enabled systems, have become commonplace. However, empirical evidence on how ML-enabled systems are engineered in practice is still limited, especially for activities surrounding ML model dissemination. [Goal] We investigate contemporary industrial practices and problems related to ML model dissemination, focusing on the…
▽ More
[Context] Systems incorporating Machine Learning (ML) models, often called ML-enabled systems, have become commonplace. However, empirical evidence on how ML-enabled systems are engineered in practice is still limited, especially for activities surrounding ML model dissemination. [Goal] We investigate contemporary industrial practices and problems related to ML model dissemination, focusing on the model deployment and the monitoring of ML life cycle phases. [Method] We conducted an international survey to gather practitioner insights on how ML-enabled systems are engineered. We gathered a total of 188 complete responses from 25 countries. We analyze the status quo and problems reported for the model deployment and monitoring phases. We analyzed contemporary practices using bootstrap** with confidence intervals and conducted qualitative analyses on the reported problems applying open and axial coding procedures. [Results] Practitioners perceive the model deployment and monitoring phases as relevant and difficult. With respect to model deployment, models are typically deployed as separate services, with limited adoption of MLOps principles. Reported problems include difficulties in designing the architecture of the infrastructure for production deployment and legacy application integration. Concerning model monitoring, many models in production are not monitored. The main monitored aspects are inputs, outputs, and decisions. Reported problems involve the absence of monitoring practices, the need to create custom monitoring tools, and the selection of suitable metrics. [Conclusion] Our results help provide a better understanding of the adopted practices and problems in practice and support guiding ML deployment and monitoring research in a problem-driven manner.
△ Less
Submitted 7 February, 2024;
originally announced February 2024.
-
Status Quo and Problems of Requirements Engineering for Machine Learning: Results from an International Survey
Authors:
Antonio Pedro Santos Alves,
Marcos Kalinowski,
Görkem Giray,
Daniel Mendez,
Niklas Lavesson,
Kelly Azevedo,
Hugo Villamizar,
Tatiana Escovedo,
Helio Lopes,
Stefan Biffl,
Jürgen Musil,
Michael Felderer,
Stefan Wagner,
Teresa Baldassarre,
Tony Gorschek
Abstract:
Systems that use Machine Learning (ML) have become commonplace for companies that want to improve their products and processes. Literature suggests that Requirements Engineering (RE) can help address many problems when engineering ML-enabled systems. However, the state of empirical evidence on how RE is applied in practice in the context of ML-enabled systems is mainly dominated by isolated case s…
▽ More
Systems that use Machine Learning (ML) have become commonplace for companies that want to improve their products and processes. Literature suggests that Requirements Engineering (RE) can help address many problems when engineering ML-enabled systems. However, the state of empirical evidence on how RE is applied in practice in the context of ML-enabled systems is mainly dominated by isolated case studies with limited generalizability. We conducted an international survey to gather practitioner insights into the status quo and problems of RE in ML-enabled systems. We gathered 188 complete responses from 25 countries. We conducted quantitative statistical analyses on contemporary practices using bootstrap** with confidence intervals and qualitative analyses on the reported problems involving open and axial coding procedures. We found significant differences in RE practices within ML projects. For instance, (i) RE-related activities are mostly conducted by project leaders and data scientists, (ii) the prevalent requirements documentation format concerns interactive Notebooks, (iii) the main focus of non-functional requirements includes data quality, model reliability, and model explainability, and (iv) main challenges include managing customer expectations and aligning requirements with data. The qualitative analyses revealed that practitioners face problems related to lack of business domain understanding, unclear goals and requirements, low customer engagement, and communication issues. These results help to provide a better understanding of the adopted practices and of which problems exist in practical environments. We put forward the need to adapt further and disseminate RE-related practices for engineering ML-enabled systems.
△ Less
Submitted 10 October, 2023;
originally announced October 2023.
-
Integrated Design Fabrication and Control of a Bioinspired Multimaterial Soft Robotic Hand
Authors:
Samuel Alves,
Mihail Babcinschi,
Afonso Silva,
Diogo Neto,
Diogo Fonseca,
Pedro Neto
Abstract:
Machines that mimic humans have inspired scientists for centuries. Bio-inspired soft robotic hands are a good example of such an endeavor, featuring intrinsic material compliance and continuous motion to deal with uncertainty and adapt to unstructured environments. Recent research led to impactful achievements in functional designs, modeling, fabrication, and control of soft robots. Nevertheless,…
▽ More
Machines that mimic humans have inspired scientists for centuries. Bio-inspired soft robotic hands are a good example of such an endeavor, featuring intrinsic material compliance and continuous motion to deal with uncertainty and adapt to unstructured environments. Recent research led to impactful achievements in functional designs, modeling, fabrication, and control of soft robots. Nevertheless, the full realization of life-like movements is still challenging to achieve, often based on trial-and-error considerations from design to fabrication, consuming time and resources. In this study, a soft robotic hand is proposed, composed of soft actuator cores and an exoskeleton, featuring a multi-material design aided by finite element analysis (FEA) to define the hand geometry and promote finger's bendability. The actuators are fabricated using molding and the exoskeleton is 3D-printed in a single step. An ON-OFF controller keeps the set fingers' inner pressures related to specific bending angles, even in the presence of leaks. The FEA numerical results were validated by experimental tests, as well as the ability of the hand to grasp objects with different shapes, weights and sizes. This integrated solution will make soft robotic hands more available to people, at a reduced cost, avoiding the time-consuming design-fabrication trial-and-error processes.
△ Less
Submitted 8 August, 2023;
originally announced August 2023.
-
Science and engineering for what? A large-scale analysis of students' projects in science fairs
Authors:
Adelmo Eloy,
Thomas Palmeira Ferraz,
Fellip Silva Alves,
Roseli de Deus Lopes
Abstract:
Science and Engineering fairs offer K-12 students opportunities to engage with authentic STEM practices. Particularly, students are given the chance to experience authentic and open inquiry processes, by defining which themes, questions and approaches will guide their scientific endeavors. In this study, we analyzed data from over 5,000 projects presented at a nationwide science fair in Brazil ove…
▽ More
Science and Engineering fairs offer K-12 students opportunities to engage with authentic STEM practices. Particularly, students are given the chance to experience authentic and open inquiry processes, by defining which themes, questions and approaches will guide their scientific endeavors. In this study, we analyzed data from over 5,000 projects presented at a nationwide science fair in Brazil over the past 20 years using topic modeling to identify the main topics that have driven students' inquiry and design. Our analysis identified a broad range of topics being explored, with significant variations over time, region, and school setting. We argue those results and proposed methodology can not only support further research in the context of science fairs, but also inform instruction and design of contexts-specific resources to support students in open inquiry experiences in different settings.
△ Less
Submitted 13 October, 2023; v1 submitted 5 August, 2023;
originally announced August 2023.
-
RobôCIn Small Size League Extended Team Description Paper for RoboCup 2023
Authors:
Aline Lima de Oliveira,
Cauê Addae da Silva Gomes,
Cecília Virginia Santos da Silva,
Charles Matheus de Sousa Alves,
Danilo Andrade Martins de Souza,
Driele Pires Ferreira Araújo Xavier,
Edgleyson Pereira da Silva,
Felipe Bezerra Martins,
Lucas Henrique Cavalcanti Santos,
Lucas Dias Maciel,
Matheus Paixão Gumercindo dos Santos,
Matheus Lafayette Vasconcelos,
Matheus Vinícius Teotonio do Nascimento Andrade,
João Guilherme Oliveira Carvalho de Melo,
João Pedro Souza Pereira de Moura,
José Ronald da Silva,
José Victor Silva Cruz,
Pedro Henrique Santana de Morais,
Pedro Paulo Salman de Oliveira,
Riei Joaquim Matos Rodrigues,
Roberto Costa Fernandes,
Ryan Vinicius Santos Morais,
Tamara Mayara Ramos Teobaldo,
Washington Igor dos Santos Silva,
Edna Natividade Silva Barros
Abstract:
RobôCIn has participated in RoboCup Small Size League since 2019, won its first world title in 2022 (Division B), and is currently a three-times Latin-American champion. This paper presents our improvements to defend the Small Size League (SSL) division B title in RoboCup 2023 in Bordeaux, France. This paper aims to share some of the academic research that our team developed over the past year. Ou…
▽ More
RobôCIn has participated in RoboCup Small Size League since 2019, won its first world title in 2022 (Division B), and is currently a three-times Latin-American champion. This paper presents our improvements to defend the Small Size League (SSL) division B title in RoboCup 2023 in Bordeaux, France. This paper aims to share some of the academic research that our team developed over the past year. Our team has successfully published 2 articles related to SSL at two high-impact conferences: the 25th RoboCup International Symposium and the 19th IEEE Latin American Robotics Symposium (LARS 2022). Over the last year, we have been continuously migrating from our past codebase to Unification. We will describe the new architecture implemented and some points of software and AI refactoring. In addition, we discuss the process of integrating machined components into the mechanical system, our development for participating in the vision blackout challenge last year and what we are preparing for this year.
△ Less
Submitted 19 July, 2023;
originally announced July 2023.
-
Quantitative Global Memory
Authors:
Sandra Alves,
Delia Kesner,
Miguel Ramos
Abstract:
We show that recent approaches of static analysis based on quantitative ty** systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs.…
▽ More
We show that recent approaches of static analysis based on quantitative ty** systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs. We show that the type system is quantitatively sound and complete with respect to the original operational semantics of the language.
△ Less
Submitted 16 June, 2023; v1 submitted 15 March, 2023;
originally announced March 2023.
-
Linear Rank Intersection Types
Authors:
Fábio Reis,
Sandra Alves,
Mário Florido
Abstract:
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to make typability decidable. One such restriction consists in using a notion of finite rank for the idempotent intersection types. In this work, we defi…
▽ More
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to make typability decidable. One such restriction consists in using a notion of finite rank for the idempotent intersection types. In this work, we define a new notion of rank for the non-idempotent intersection types. We then define a novel type system and a type inference algorithm for the lambda-calculus, using the new notion of rank 2. In the second part of this work, we extend the type system and the type inference algorithm to use the quantitative properties of the non-idempotent intersection types to infer quantitative information related to resource usage.
△ Less
Submitted 4 May, 2023; v1 submitted 30 November, 2022;
originally announced November 2022.
-
Intuitive Robot Programming by Capturing Human Manufacturing Skills: A Framework for the Process of Glass Adhesive Application
Authors:
Mihail Babcinschi,
Francisco Cruz,
Nicole Duarte,
Silvia Santos,
Samuel Alves,
Pedro Neto
Abstract:
There is a great demand for the robotization of manufacturing processes fea-turing monotonous labor. Some manufacturing tasks requiring specific skills (welding, painting, etc.) suffer from a lack of workers. Robots have been used in these tasks, but their flexibility is limited since they are still difficult to program/re-program by non-experts, making them inaccessible to most companies. Robot o…
▽ More
There is a great demand for the robotization of manufacturing processes fea-turing monotonous labor. Some manufacturing tasks requiring specific skills (welding, painting, etc.) suffer from a lack of workers. Robots have been used in these tasks, but their flexibility is limited since they are still difficult to program/re-program by non-experts, making them inaccessible to most companies. Robot offline programming (OLP) is reliable. However, generat-ed paths directly from CAD/CAM do not include relevant parameters repre-senting human skills such as robot end-effector orientations and velocities. This paper presents an intuitive robot programming system to capture human manufacturing skills and transform them into robot programs. Demonstra-tions from human skilled workers are recorded using a magnetic tracking system attached to the worker tools. Collected data include the orientations and velocity of the working paths. Positional data are extracted from CAD/CAM since its error when captured by the magnetic tracker, is signifi-cant. Paths poses are transformed in Cartesian space and validated in a simu-lation environment. Robot programs are generated and transferred to the real robot. Experiments on the process of glass adhesive application demonstrat-ed the intuitiveness to use and effectiveness of the proposed framework in capturing human skills and transferring them to the robot.
△ Less
Submitted 15 September, 2022;
originally announced September 2022.
-
Evaluation of Different Annotation Strategies for Deployment of Parking Spaces Classification Systems
Authors:
Andre G. Hochuli,
Alceu S. Britto Jr.,
Paulo R. L. de Almeida,
Williams B. S. Alves,
Fabio M. C. Cagni
Abstract:
When using vision-based approaches to classify individual parking spaces between occupied and empty, human experts often need to annotate the locations and label a training set containing images collected in the target parking lot to fine-tune the system. We propose investigating three annotation types (polygons, bounding boxes, and fixed-size squares), providing different data representations of…
▽ More
When using vision-based approaches to classify individual parking spaces between occupied and empty, human experts often need to annotate the locations and label a training set containing images collected in the target parking lot to fine-tune the system. We propose investigating three annotation types (polygons, bounding boxes, and fixed-size squares), providing different data representations of the parking spaces. The rationale is to elucidate the best trade-off between handcraft annotation precision and model performance. We also investigate the number of annotated parking spaces necessary to fine-tune a pre-trained model in the target parking lot. Experiments using the PKLot dataset show that it is possible to fine-tune a model to the target parking lot with less than 1,000 labeled samples, using low precision annotations such as fixed-size squares.
△ Less
Submitted 22 July, 2022;
originally announced July 2022.
-
Should Social Robots in Retail Manipulate Customers?
Authors:
Oliver Bendel,
Liliana Margarida Dos Santos Alves
Abstract:
Against the backdrop of structural changes in the retail trade, social robots have found their way into retail stores and shop** malls in order to attract, welcome, and greet customers; to inform them, advise them, and persuade them to make a purchase. Salespeople often have a broad knowledge of their product and rely on offering competent and honest advice, whether it be on shoes, clothing, or…
▽ More
Against the backdrop of structural changes in the retail trade, social robots have found their way into retail stores and shop** malls in order to attract, welcome, and greet customers; to inform them, advise them, and persuade them to make a purchase. Salespeople often have a broad knowledge of their product and rely on offering competent and honest advice, whether it be on shoes, clothing, or kitchen appliances. However, some frequently use sales tricks to secure purchases. The question arises of how consulting and sales robots should "behave". Should they behave like human advisors and salespeople, i.e., occasionally manipulate customers? Or should they be more honest and reliable than us? This article tries to answer these questions. After explaining the basics, it evaluates a study in this context and gives recommendations for companies that want to use consulting and sales robots. Ultimately, fair, honest, and trustworthy robots in retail are a win-win situation for all concerned.
△ Less
Submitted 17 June, 2022;
originally announced June 2022.
-
Structural Rules and Algebraic Properties of Intersection Types
Authors:
Sandra Alves,
Mário Florido
Abstract:
In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. Expansion relates terms typed by associative, commutative and idempotent intersections with terms typed in the Curry type system and the relevant type system, terms typed by non-idempotent intersections with t…
▽ More
In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. Expansion relates terms typed by associative, commutative and idempotent intersections with terms typed in the Curry type system and the relevant type system, terms typed by non-idempotent intersections with terms typed in the affine and linear type systems and terms typed by non-idempotent and non-commutative intersections with terms typed in an ordered type system. Finally, we show how idempotent intersection is related with the contraction rule, commutative intersection with the exchange rule and associative intersection with the lack of structural rules in a type system.
△ Less
Submitted 3 May, 2022; v1 submitted 26 April, 2022;
originally announced April 2022.
-
A Graphical Framework for the Category-Based Metamodel for Access Control and Obligations
Authors:
Sandra Alves,
Jorge Iglésias
Abstract:
We design a graph-based framework for the visualisation and analysis of obligations in access control policies. We consider obligation policies in CBACO, the category-based access control model, which has been shown to subsume many of the most well known access control such as MAC, DAC, RBAC. CBACO is an extension of the CBAC metamodel that deals with obligations. We describe the implementation of…
▽ More
We design a graph-based framework for the visualisation and analysis of obligations in access control policies. We consider obligation policies in CBACO, the category-based access control model, which has been shown to subsume many of the most well known access control such as MAC, DAC, RBAC. CBACO is an extension of the CBAC metamodel that deals with obligations. We describe the implementation of the proposed model in PORGY, a strategy driven graph-rewriting tool, based on the theory of port-graphs. CBACO policies allow for dynamic behavior in the modelled systems, which is implemented using the strategy language of PORGY.
△ Less
Submitted 31 October, 2021;
originally announced November 2021.
-
EVL: a typed functional language for event processing
Authors:
Sandra Alves,
Maribel Fernández,
Miguel Ramos
Abstract:
We define EVL, a minimal higher-order functional language to deal with generic events. The notion of generic event extends the well-known notion of event traditionally used in a variety of areas, such as database management, concurrency, reactive systems and cybersecurity. Generic events were introduced in the context of a metamodel to specify obligations in access control systems. Event specifica…
▽ More
We define EVL, a minimal higher-order functional language to deal with generic events. The notion of generic event extends the well-known notion of event traditionally used in a variety of areas, such as database management, concurrency, reactive systems and cybersecurity. Generic events were introduced in the context of a metamodel to specify obligations in access control systems. Event specifications are represented as records and we use polymorphic record types to type events in EVL. We show how the higher-order capabilities of EVL can be used in the context of Complex Event Processing (CEP), to define higher-order parameterised functions that deal with the usual CEP techniques.
△ Less
Submitted 28 October, 2021; v1 submitted 18 September, 2021;
originally announced September 2021.
-
An ML-style Record Calculus with Extensible Records
Authors:
Sandra Alves,
Miguel Ramos
Abstract:
In this work, we develop a polymorphic record calculus with extensible records. Extensible records are records that can have new fields added to them, or preexisting fields removed from them. We also develop a static type system for this calculus and a sound and complete type inference algorithm. Most ML-style polymorphic record calculi that support extensible records are based on row variables. W…
▽ More
In this work, we develop a polymorphic record calculus with extensible records. Extensible records are records that can have new fields added to them, or preexisting fields removed from them. We also develop a static type system for this calculus and a sound and complete type inference algorithm. Most ML-style polymorphic record calculi that support extensible records are based on row variables. We present an alternative construction based on the polymorphic record calculus developed by Ohori. Ohori based his polymorphic record calculus on the idea of kind restrictions. This allowed him to express polymorphic operations on records such as field selection and modification. With the addition of extensible types, we were able to extend Ohori's original calculus with other powerful operations on records such as field addition and removal.
△ Less
Submitted 28 December, 2021; v1 submitted 13 August, 2021;
originally announced August 2021.
-
A Quantitative Understanding of Pattern Matching
Authors:
Sandra Alves,
Delia Kesner,
Daniel Ventura
Abstract:
This paper shows that the recent approach to quantitative ty** systems for programming languages can be extended to pattern matching features. Indeed, we define two resource aware type systems, named U and E, for a lambda-calculus equipped with pairs for both patterns and terms. Our ty** systems borrow some basic ideas from [BKRDR15], which characterises (head) normalisation in a qualitative w…
▽ More
This paper shows that the recent approach to quantitative ty** systems for programming languages can be extended to pattern matching features. Indeed, we define two resource aware type systems, named U and E, for a lambda-calculus equipped with pairs for both patterns and terms. Our ty** systems borrow some basic ideas from [BKRDR15], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But in contrast to [BKRDR15], our (static) systems also provides quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs, instead of the disjoint unions in [BKRDR15], thus avoiding an overlap between "being a pair" and "being duplicable", resulting in an essential tool to reason about quantitativity. Secondly, ty** sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (c.f. length) and space (c.f. size). Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors. Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta reduction, substitution and matching steps are counted separately.
△ Less
Submitted 4 December, 2019;
originally announced December 2019.
-
Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems
Authors:
Michele Pagani,
Sandra Alves
Abstract:
This volume contains a final and revised selection of papers presented at Twelfth Workshop on Developments in Computational Models (DCM 2018) and the Ninth Workshop on Intersection Types and Related Systems (ITRS 2018), held on July 8, 2018 in Oxford, in affiliation with FLOC 2018.
This volume contains a final and revised selection of papers presented at Twelfth Workshop on Developments in Computational Models (DCM 2018) and the Ninth Workshop on Intersection Types and Related Systems (ITRS 2018), held on July 8, 2018 in Oxford, in affiliation with FLOC 2018.
△ Less
Submitted 21 April, 2019;
originally announced April 2019.
-
Polynomial Invariant Theory and Shape Enumerator of Self-Dual Codes in the NRT-Metric
Authors:
Welington Santos,
Marcelo Muniz Silva Alves
Abstract:
In this paper we consider self-dual NRT-codes, that is, self-dual codes in the metric space endowed with the Niederreiter-Rosenbloom-Tsfasman (NRT-metric). We use polynomial invariant theory to describe the shape enumerator of a binary self-dual, doubly even self-dual, and doubly-doubly even self dual NRT-code $C\subseteq M_{n,2}(\mathbb{F}_{2})$. Motivated by these results we describe the number…
▽ More
In this paper we consider self-dual NRT-codes, that is, self-dual codes in the metric space endowed with the Niederreiter-Rosenbloom-Tsfasman (NRT-metric). We use polynomial invariant theory to describe the shape enumerator of a binary self-dual, doubly even self-dual, and doubly-doubly even self dual NRT-code $C\subseteq M_{n,2}(\mathbb{F}_{2})$. Motivated by these results we describe the number of invariant polinomials that we must find to describe the shape enumerator of a self-dual NRT-code of $M_{n,s}(\mathbb{F}_{2})$. We define the ordered flip of a matrix $A\in M_{k,ns}(\mathbb{F}_{q})$ and present some constructions of self-dual NRT-codes over $\mathbb{F}_{q}$. We further give an application of ordered flip to the classification of bidimensional self-dual NRT-codes.
△ Less
Submitted 8 April, 2019;
originally announced April 2019.
-
The dangerous path towards your own cryptography method
Authors:
Warley M. S. Alves,
Thiago L. Prado,
Antonio M. Batista,
Fabiano A. S. Ferrari
Abstract:
Would you like to have your own cryptography method? Experts say you should not do it. If you think you can develop a better cryptography method anyway. We present a brief discussion about some well known cryptography methods and how our model fails against the traditional attacks. We do not want to discourage anybody, we just want to show that, despite of the importance of develo** better crypt…
▽ More
Would you like to have your own cryptography method? Experts say you should not do it. If you think you can develop a better cryptography method anyway. We present a brief discussion about some well known cryptography methods and how our model fails against the traditional attacks. We do not want to discourage anybody, we just want to show that, despite of the importance of develo** better cryptography models, it is a very hard task.
△ Less
Submitted 26 September, 2018;
originally announced December 2018.
-
On the (parameterized) complexity of recognizing well-covered (r,l)-graphs
Authors:
Sancrey R. Alves,
Konrad K. Dabrowski,
Luerbio Faria,
Sulamita Klein,
Ignasi Sau,
Uéverton S. Souza
Abstract:
An $(r, \ell)$-partition of a graph $G$ is a partition of its vertex set into $r$ independent sets and $\ell$ cliques. A graph is $(r, \ell)$ if it admits an $(r, \ell)$-partition. A graph is well-covered if every maximal independent set is also maximum. A graph is $(r,\ell)$-well-covered if it is both $(r,\ell)$ and well-covered. In this paper we consider two different decision problems. In the…
▽ More
An $(r, \ell)$-partition of a graph $G$ is a partition of its vertex set into $r$ independent sets and $\ell$ cliques. A graph is $(r, \ell)$ if it admits an $(r, \ell)$-partition. A graph is well-covered if every maximal independent set is also maximum. A graph is $(r,\ell)$-well-covered if it is both $(r,\ell)$ and well-covered. In this paper we consider two different decision problems. In the $(r,\ell)$-Well-Covered Graph problem ($(r,\ell)$WCG for short), we are given a graph $G$, and the question is whether $G$ is an $(r,\ell)$-well-covered graph. In the Well-Covered $(r,\ell)$-Graph problem (WC$(r,\ell)$G for short), we are given an $(r,\ell)$-graph $G$ together with an $(r,\ell)$-partition of $V(G)$ into $r$ independent sets and $\ell$ cliques, and the question is whether $G$ is well-covered. We classify most of these problems into P, coNP-complete, NP-complete, NP-hard, or coNP-hard. Only the cases WC$(r,0)$G for $r\geq 3$ remain open. In addition, we consider the parameterized complexity of these problems for several choices of parameters, such as the size $α$ of a maximum independent set of the input graph, its neighborhood diversity, its clique-width, or the number $\ell$ of cliques in an $(r, \ell)$-partition. In particular, we show that the parameterized problem of deciding whether a general graph is well-covered parameterized by $α$ can be reduced to the WC$(0,\ell)$G problem parameterized by $\ell$. In addition, we prove that both problems are coW[2]-hard but can be solved in XP-time.
△ Less
Submitted 6 June, 2018; v1 submitted 25 May, 2017;
originally announced May 2017.
-
The G-ACM Tool: using the Drools Rule Engine for Access Control Management
Authors:
João Sá,
Sandra Alves,
Sabine Broda
Abstract:
In this paper we explore the usage of rule engines in a graphical framework for visualising dynamic access control policies. We use the Drools rule engine to dynamically compute permissions, following the Category-Based Access Control metamodel.
In this paper we explore the usage of rule engines in a graphical framework for visualising dynamic access control policies. We use the Drools rule engine to dynamically compute permissions, following the Category-Based Access Control metamodel.
△ Less
Submitted 25 November, 2016;
originally announced November 2016.
-
Burstiness Scale: a highly parsimonious model for characterizing random series of events
Authors:
Rodrigo A S Alves,
Renato Assunção,
Pedro O S Vaz de Melo
Abstract:
The problem to accurately and parsimoniously characterize random series of events (RSEs) present in the Web, such as e-mail conversations or Twitter hashtags, is not trivial. Reports found in the literature reveal two apparent conflicting visions of how RSEs should be modeled. From one side, the Poissonian processes, of which consecutive events follow each other at a relatively regular time and sh…
▽ More
The problem to accurately and parsimoniously characterize random series of events (RSEs) present in the Web, such as e-mail conversations or Twitter hashtags, is not trivial. Reports found in the literature reveal two apparent conflicting visions of how RSEs should be modeled. From one side, the Poissonian processes, of which consecutive events follow each other at a relatively regular time and should not be correlated. On the other side, the self-exciting processes, which are able to generate bursts of correlated events and periods of inactivities. The existence of many and sometimes conflicting approaches to model RSEs is a consequence of the unpredictability of the aggregated dynamics of our individual and routine activities, which sometimes show simple patterns, but sometimes results in irregular rising and falling trends. In this paper we propose a highly parsimonious way to characterize general RSEs, namely the Burstiness Scale (BuSca) model. BuSca views each RSE as a mix of two independent process: a Poissonian and a self-exciting one. Here we describe a fast method to extract the two parameters of BuSca that, together, gives the burstyness scale, which represents how much of the RSE is due to bursty and viral effects. We validated our method in eight diverse and large datasets containing real random series of events seen in Twitter, Yelp, e-mail conversations, Digg, and online forums. Results showed that, even using only two parameters, BuSca is able to accurately describe RSEs seen in these diverse systems, what can leverage many applications.
△ Less
Submitted 20 February, 2016;
originally announced February 2016.
-
On cyclotomic cosets and code constructions
Authors:
Giuliano Gadioli La Guardia,
Marcelo Muniz Silva Alves
Abstract:
New properties of $q$-ary cyclotomic cosets modulo $n = q^{m} - 1$, where $q \geq 3$ is a prime power, are investigated in this paper. Based on these properties, the dimension as well as bounds for the designed distance of some families of classical cyclic codes can be computed. As an application, new families of nonbinary Calderbank-Shor-Steane (CSS) quantum codes as well as new families of convo…
▽ More
New properties of $q$-ary cyclotomic cosets modulo $n = q^{m} - 1$, where $q \geq 3$ is a prime power, are investigated in this paper. Based on these properties, the dimension as well as bounds for the designed distance of some families of classical cyclic codes can be computed. As an application, new families of nonbinary Calderbank-Shor-Steane (CSS) quantum codes as well as new families of convolutional codes are constructed in this work. These new CSS codes have parameters better than the ones available in the literature. The convolutional codes constructed here have free distance greater than the ones available in the literature.
△ Less
Submitted 12 November, 2015;
originally announced November 2015.
-
Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)
Authors:
Erickson H. da S. Alves,
Lucas C. Cordeiro,
Eddie B. de Lima Filho
Abstract:
Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threa…
▽ More
Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threaded program into a corresponding sequential one and then uses a fault-diagnosis method suitable for this type of program, in order to localize faults. The code transformation is implemented with rules and context switch information from counterexamples, which are typically generated by bounded model checkers. Experimental results show that the proposed method is effective, in such a way that sequential fault-localization methods can be extended to multi-threaded programs.
△ Less
Submitted 8 September, 2015;
originally announced September 2015.
-
Liquid Intersection Types
Authors:
Mário Pereira,
Sandra Alves,
Mário Florido
Abstract:
We present a new type system combining refinement types and the expressiveness of intersection type discipline. The use of such features makes it possible to derive more precise types than in the original refinement system. We have been able to prove several interesting properties for our system (including subject reduction) and developed an inference algorithm, which we proved to be sound.
We present a new type system combining refinement types and the expressiveness of intersection type discipline. The use of such features makes it possible to derive more precise types than in the original refinement system. We have been able to prove several interesting properties for our system (including subject reduction) and developed an inference algorithm, which we proved to be sound.
△ Less
Submitted 16 March, 2015;
originally announced March 2015.
-
Proceedings Third International Workshop on Linearity
Authors:
Sandra Alves,
Iliano Cervesato
Abstract:
This volume contains the papers presented at LINEARITY 2014, the Third International Workshop on Linearity, held on July 13, 2014 in Vienna, Austria. The workshop was a one-day satellite event of FLoC 2014, the sixth Federated Logic Conference. It was held as part of the 2014 Vienna Summer of Logic.
The aim of this workshop was to bring together researchers who are exploring theory and applica…
▽ More
This volume contains the papers presented at LINEARITY 2014, the Third International Workshop on Linearity, held on July 13, 2014 in Vienna, Austria. The workshop was a one-day satellite event of FLoC 2014, the sixth Federated Logic Conference. It was held as part of the 2014 Vienna Summer of Logic.
The aim of this workshop was to bring together researchers who are exploring theory and applications of linear calculi, to foster their interaction and provide a forum for presenting new ideas and work in progress, and enable newcomers to learn about current activities in this area. Of interest were new results that made a central use of linearity, ranging from foundational work to applications in any field. This included: sub-linear logics, linear term calculi, linear type systems, linear proof-theory, linear programming languages, applications to concurrency, interaction-based systems, verification of linear systems, quantum models of computation, and biological and chemical models of computation.
△ Less
Submitted 15 February, 2015;
originally announced February 2015.
-
Proceedings 2nd International Workshop on Linearity
Authors:
Sandra Alves,
Ian Mackie
Abstract:
This volume contains a selection of the papers presented at the 2nd International Workshop on Linearity (LINEARITY'2012), which took place 1 April 2012 in Tallinn, Estonia. The workshop was a one-day satellite event of ETAPS 2012, the 15th European Joint Conference on Theory and Practice of Software.
The aim of this workshop was to bring together researchers who are currently develo** theory a…
▽ More
This volume contains a selection of the papers presented at the 2nd International Workshop on Linearity (LINEARITY'2012), which took place 1 April 2012 in Tallinn, Estonia. The workshop was a one-day satellite event of ETAPS 2012, the 15th European Joint Conference on Theory and Practice of Software.
The aim of this workshop was to bring together researchers who are currently develo** theory and applications of linear calculi, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area.
△ Less
Submitted 14 November, 2012;
originally announced November 2012.
-
A standard form for generator matrices with respect to the Niederreiter-Rosenbloom-Tsfasman metric
Authors:
Marcelo Muniz S. Alves
Abstract:
In this note, we present an analogue for codes in vector spaces with a Rosenbloom-Tsfasman metric of the well-known standard form of generator matrices for codes in spaces with the Hamming metric.
In this note, we present an analogue for codes in vector spaces with a Rosenbloom-Tsfasman metric of the well-known standard form of generator matrices for codes in spaces with the Hamming metric.
△ Less
Submitted 11 May, 2011;
originally announced May 2011.
-
A new graphical calculus of proofs
Authors:
Sandra Alves,
Maribel Fernández,
Ian Mackie
Abstract:
We offer a simple graphical representation for proofs of intuitionistic logic, which is inspired by proof nets and interaction nets (two formalisms originating in linear logic). This graphical calculus of proofs inherits good features from each, but is not constrained by them. By the Curry-Howard isomorphism, the representation applies equally to the lambda calculus, offering an alternative diagra…
▽ More
We offer a simple graphical representation for proofs of intuitionistic logic, which is inspired by proof nets and interaction nets (two formalisms originating in linear logic). This graphical calculus of proofs inherits good features from each, but is not constrained by them. By the Curry-Howard isomorphism, the representation applies equally to the lambda calculus, offering an alternative diagrammatic representation of functional computations.
△ Less
Submitted 13 February, 2011;
originally announced February 2011.
-
Linear Recursion
Authors:
Sandra Alves,
Maribel Fernández,
Mário Florido,
Ian Mackie
Abstract:
We define two extensions of the typed linear lambda-calculus that yield minimal Turing-complete systems. The extensions are based on unbounded recursion in one case, and bounded recursion with minimisation in the other. We show that both approaches are compatible with linearity and typeability constraints. Both extensions of the typed linear lambda-calculus are minimal, in the sense that taking ou…
▽ More
We define two extensions of the typed linear lambda-calculus that yield minimal Turing-complete systems. The extensions are based on unbounded recursion in one case, and bounded recursion with minimisation in the other. We show that both approaches are compatible with linearity and typeability constraints. Both extensions of the typed linear lambda-calculus are minimal, in the sense that taking out any of the components breaks the universality of the system. We discuss implementation techniques that exploit the linearity of the calculi. Finally, we apply the results to languages with fixpoint operators: we give a compilation of the programming language PCF into a linear lambda-calculus with linear unbounded recursion.
△ Less
Submitted 25 November, 2016; v1 submitted 19 January, 2010;
originally announced January 2010.
-
The Symmetries of the $π$-metric
Authors:
Marcelo Muniz S. Alves,
Luciano Panek
Abstract:
Let V be an n-dimensional vector space over a finite field F_q. We consider on V the $π$-metric recently introduced by K. Feng, L. Xu and F. J. Hickernell. In this short note we give a complete description of the group of symmetries of V under the $π$-metric.
Let V be an n-dimensional vector space over a finite field F_q. We consider on V the $π$-metric recently introduced by K. Feng, L. Xu and F. J. Hickernell. In this short note we give a complete description of the group of symmetries of V under the $π$-metric.
△ Less
Submitted 8 January, 2009;
originally announced January 2009.
