Searcharxiv⌕ Search

arXiv subjects

Manuel Mazzara

Publications and source records attributed to Manuel Mazzara.

At least 73 records · Page 4Linked to original sources

Hikester - the event management application

Today social networks and services are one of the most important part of our everyday life. Most of the daily activities, such as communicating with friends, reading news or dating is usually done using social networks. However, there are activities for which social networks do not yet provide adequate support. This paper focuses on event management and introduces "Hikester". The main objective of this service is to provide users with the possibility to create any event they desire and to invite other users. "Hikester" supports the creation and management of events like attendance of football matches, quest rooms, shared train rides or visit of museums in foreign countries. Here we discuss the project architecture as well as the detailed implementation of the system components: the recommender system, the spam recognition service and the parameters optimizer.

cs.SI↗

Towards dynamic interaction-based model

In this paper, we investigate how dynamic properties of reputation can influence the quality of users ranking. Reputation systems should be based on rules that can guarantee a high level of trust and help identifying unreliable units. To understand the effectiveness of dynamic properties in the evaluation of reputation, we propose our own model (DIB-RM) that is based on three factors: forgetting, cumulative, and activity period. In order to evaluate the model, we use data from StackOverflow, which also has its own reputation model. We estimate similarity of ratings between DIB-RM and the StackOverflow model so to check our hypothesis. We use two values to calculate our metric: DIB-RM reputation and $historical$ reputation. We found that $historical$ reputation gives better metric values. Our preliminary results are presented for different sets of values of the aforementioned factors in order to analyze how effectively the model can be used for modeling reputation systems.

cs.SI↗

Model Checking in multiplayer games development

Multiplayer computer games play a big role in the ever-growing entertainment industry. Being competitive in this industry means releasing the best possible software, and reliability is a key feature to win the market. Computer games are also actively used to simulate different robotic systems where reliability is even more important, and potentially critical. Traditional software testing approaches can check a subset of all the possible program executions, and they can never guarantee complete absence of errors in the source code. On the other hand, during more than twenty years, Model Checking has demonstrated to be a powerful instrument for formal verification of large hardware and software components. In this paper, we contribute with a novel approach to formally verify computer games. We propose a method of model construction that starts from a computer game description and utilizes Model Checking technique. We apply the method on a case study: the game Penguin Clash. Finally, an approach to game model reduction (and its implementation) is introduced in order to address the state explosion problem.

cs.SE↗

Jolie Static Type Checker: a prototype

Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both static and dynamic type checking. With such approach, the static type checker verifies everything possible at compile time, and dynamic checks the remaining. The current state of the Jolie programming language includes a dynamic type system. Consequently, it allows avoidable run-time errors. A static type system for the language has been formally defined on paper but lacks an implementation yet. In this paper, we describe a prototype of Jolie Static Type Checker (JSTC), which employs a technique based on a SMT solver. We describe the theory behind and the implementation, and the process of static analysis.

cs.SE↗

Domain Objects and Microservices for Systems Development: a roadmap

This paper discusses a roadmap to investigate Domain Objects being an adequate formalism to capture the peculiarity of microservice architecture, and to support Software development since the early stages. It provides a survey of both Microservices and Domain Objects, and it discusses plans and reflections on how to investigate whether a modeling approach suited to adaptable service-based components can also be applied with success to the microservice scenario.

cs.SE↗

Joining Jolie to Docker - Orchestration of Microservices on a Containers-as-a-Service Layer

Cloud computing is steadily growing and, as IaaS vendors have started to offer pay-as-you-go billing policies, it is fundamental to achieve as much elasticity as possible, avoiding over-provisioning that would imply higher costs. In this paper, we briefly analyse the orchestration characteristics of PaaSSOA, a proposed architecture already implemented for Jolie microservices, and Kubernetes, one of the various orchestration plugins for Docker; then, we outline similarities and differences of the two approaches, with respect to their own domain of application. Furthermore, we investigate some ideas to achieve a federation of the two technologies, proposing an architectural composition of Jolie microservices on Docker Container-as-a-Service layer.

cs.SE↗

The Internet of Hackable Things

The Internet of Things makes possible to connect each everyday object to the Internet, making computing pervasive like never before. From a security and privacy perspective, this tsunami of connectivity represents a disaster, which makes each object remotely hackable. We claim that, in order to tackle this issue, we need to address a new challenge in security: education.

cs.CR↗

AntibIoTic: Protecting IoT Devices Against DDoS Attacks

The 2016 is remembered as the year that showed to the world how dangerous Distributed Denial of Service attacks can be. Gauge of the disruptiveness of DDoS attacks is the number of bots involved: the bigger the botnet, the more powerful the attack. This character, along with the increasing availability of connected and insecure IoT devices, makes DDoS and IoT the perfect pair for the malware industry. In this paper we present the main idea behind AntibIoTic, a palliative solution to prevent DDoS attacks perpetrated through IoT devices.

cs.CR↗

Microservices Science and Engineering

In this paper we offer an overview on the topic of Microservices Science and Engineering (MSE) and we provide a collection of bibliographic references and links relevant to understand an emerging field. We try to clarify some misunderstandings related to microservices and Service-Oriented Architectures, and we also describe projects and applications our team have been working on in the recent past, both regarding programming languages construction and intelligent buildings.

cs.SE↗

Initial steps towards assessing the usability of a verification tool

In this paper we report the experience of using AutoProof to statically verify a small object oriented program. We identified the problems that emerged by this activity and we classified them according to their nature. In particular, we distinguish between tool-related and methodology-related issues, and propose necessary changes to simplify both tool and method.

cs.SE↗

Self-adaptive node-based PCA encodings

In this paper we propose an algorithm, Simple Hebbian PCA, and prove that it is able to calculate the principal component analysis (PCA) in a distributed fashion across nodes. It simplifies existing network structures by removing intralayer weights, essentially cutting the number of weights that need to be trained in half.

cs.NE↗

Translating Event-B machines to Eiffel programs

Formal modelling languages play a key role in the development of software since they enable users to prove correctness of system properties. However, there is still not a clear understanding on how to map a formal model to a specific programming language. In order to propose a solution, this paper presents a source-to-source mapping between Event- B models and Eiffel programs, therefore enabling the proof of correctness of certain system properties via Design-by-Contract (natively supported by Eiffel), while still making use of all features of O-O programming.

cs.SE↗

Microservices: a Language-based Approach

Microservices is an emerging development paradigm where software is obtained by composing autonomous entities, called (micro)services. However, microservice systems are currently developed using general-purpose programming languages that do not provide dedicated abstractions for service composition. Instead, current practice is focused on the deployment aspects of microservices, in particular by using containerization. In this chapter, we make the case for a language-based approach to the engineering of microservice architectures, which we believe is complementary to current practice. We discuss the approach in general, and then we instantiate it in terms of the Jolie programming language.

cs.PL↗

Microservices: yesterday, today, and tomorrow

Microservices is an architectural style inspired by service-oriented computing that has recently started gaining popularity. Before presenting the current state-of-the-art in the field, this chapter reviews the history of software architecture, the reasons that led to the diffusion of objects and services first, and microservices later. Finally, open problems and future challenges are introduced. This survey primarily addresses newcomers to the discipline, while offering an academic viewpoint on the topic. In addition, we investigate some practical issues and point out some potential solutions.

cs.SE↗

A contract-based method to specify stimulus-response requirements

A number of formal methods exist for capturing stimulus-response requirements in a declarative form. Someone yet needs to translate the resulting declarative statements into imperative programs. The present article describes a method for specification and verification of stimulus-response requirements in the form of imperative program routines with conditionals and assertions. A program prover then checks a candidate program directly against the stated requirements. The article illustrates the approach by applying it to an ASM model of the Landing Gear System, a widely used realistic example proposed for evaluating specification and verification techniques.

cs.SE↗

Pseudorehearsal in actor-critic agents

Catastrophic forgetting has a serious impact in reinforcement learning, as the data distribution is generally sparse and non-stationary over time. The purpose of this study is to investigate whether pseudorehearsal can increase performance of an actor-critic agent with neural-network based policy selection and function approximation in a pole balancing task and compare different pseudorehearsal approaches. We expect that pseudorehearsal assists learning even in such very simple problems, given proper initialization of the rehearsal parameters.

cs.AI↗

Microservices: Migration of a Mission Critical System

The microservices paradigm aims at changing the way in which software is perceived, conceived and designed. One of the foundational characteristics of this new promising paradigm, compared for instance to monolithic architectures, is scalability. In this paper, we present a real world case study in order to demonstrate how scalability is positively affected by re-implementing a monolithic architecture into microservices. The case study is based on the FX Core system, a mission critical system of Danske Bank, the largest bank in Denmark and one of the leading financial institutions in Northern Europe.

cs.SE↗

Link Prediction using Top-$k$ Shortest Distances

In this paper, we apply an efficient top-$k$ shortest distance routing algorithm to the link prediction problem and test its efficacy. We compare the results with other base line and state-of-the-art methods as well as with the shortest path. Our results show that using top-$k$ distances as a similarity measure outperforms classical similarity measures such as Jaccard and Adamic/Adar.

cs.SI↗