arXiv subjects

Manuel Mazzara

Publications and source records attributed to Manuel Mazzara.

107 records · Page 6Linked to original sources

arXiv2016

Towards Anthropo-inspired Computational Systems: the $P^3$ Model

This paper proposes a model which aim is providing a more coherent framework for agents design. We identify three closely related anthropo-centered domains working on separate functional levels. Abstracting from human physiology, psychology, and philosophy we create the $P^3$ model to be used as a multi-tier approach to deal with complex class of problems. The three layers identified in this model have been named PhysioComputing, MindComputing, and MetaComputing. Several instantiations of this model are finally presented related to different IT areas such as artificial intelligence, distributed computing, software and service engineering.

cs.AI↗

arXiv2016

A Cognitive Architecture for the Implementation of Emotions in Computing Systems

In this paper we present a new neurobiologically-inspired affective cognitive architecture: NEUCOGAR (NEUromodulating COGnitive ARchitecture). The objective of NEUCOGAR is the identification of a mapping from the influence of serotonin, dopamine and noradrenaline to the computing processes based on Von Neuman's architecture, in order to implement affective phenomena which can operate on the Turing's machine model. As basis of the modeling we use and extend the Lövheim Cube of Emotion with parameters of the Von Neumann architecture. Validation is conducted via simulation on a computing system of dopamine neuromodulation and its effects on the Cortex. In the experimental phase of the project, the increase of computing power and storage redistribution due to emotion stimulus modulated by the dopamine system, confirmed the soundness of the model.

cs.AI↗

arXiv2016

Usability of AutoProof: a case study of software verification

Many verification tools come out of academic projects, whose natural constraints do not typically lead to a strong focus on usability. For widespread use, however, usability is essential. Using a well-known benchmark, the Tokeneer problem, we evaluate the usability of a recent and promising verification tool: AutoProof. The results show the efficacy of the tool in verifying a real piece of software and automatically discharging nearly two thirds of verification conditions. At the same time, the case study shows the demand for improved documentation and emphasizes the need for improvement in the tool itself and in the Eiffel IDE.

cs.SE↗

arXiv2016

Robot Dream

In this position paper we present a novel approach to neurobiologically plausible implementation of emotional reactions and behaviors for real-time autonomous robotic systems. The working metaphor we use is the "day" and "night" phases of mammalian life. During the "day" phase a robotic system stores the inbound information and is controlled by a light-weight rule-based system in real time. In contrast to that, during the "night" phase the stored information is been transferred to the supercomputing system to update the realistic neural network: emotional and behavioral strategies.

cs.RO↗

arXiv2016

Quality Attributes in Practice: Contemporary Data

It is well known that the software process in place impacts the quality of the resulting product. However, the specific way in which this effect occurs is still mostly unknown and reported through anecdotes. To gather a better understanding of such relationship, a very large survey has been conducted during the last year and has been completed by more than 100 software developers and engineers from 21 countries. We have used the percentage of satisfied customers estimated by the software developers and engineers as the main dependent variable. The results evidence some interesting patterns, like that quality attribute of which customers are more satisfied appears functionality, architectural styles may not have a significant influence on quality, agile methodologies might result in happier customers, larger companies and shorter projects seems to produce better products.

cs.SE↗

arXiv2016

Refinement types in Jolie

Jolie is the first language for microservices and it is currently dynamically type checked. This paper considers the opportunity to integrate dynamic and static type checking with the introduction of refinement types, verified via SMT solver. The integration of the two aspects allows a scenario where the static verification of internal services and the dynamic verification of (potentially malicious) external services cooperates in order to reduce testing effort and enhancing security.

cs.SE↗

arXiv2015

Data-driven Workflows for Microservices

Microservices is an architectural style inspired by service-oriented computing that has recently started gaining popularity. Jolie is a programming language based on the microservices paradigm: the main building block of Jolie systems are services, in contrast to, e.g., functions or objects. The primitives offered by the Jolie language elicit many of the recurring patterns found in microservices, like load balancers and structured processes. However, Jolie still lacks some useful constructs for dealing with message types and data manipulation that are present in service-oriented computing. In this paper, we focus on the possibility of expressing choices at the level of data types, a feature well represented in standards for Web Services, e.g., WSDL. We extend Jolie to support such type choices and show the impact of our implementation on some of the typical scenarios found in microservice systems. This shows how computation can move from a process-driven to a data-driven approach, and leads to the preliminary identification of recurring communication patterns that can be shaped as design patterns.

cs.PL↗

arXiv2014

Proceedings First Workshop on Logics and Model-checking for Self-* Systems

This volume contains the proceedings of the First Workshop on Logics and Model-checking for self-* systems (MOD* 2014). The worshop took place in Bertinoro, Italy, on 12th of September 2014, and was a satellite event of iFM 2014 (the 11th International Conference on Integrated Formal Methods). The workshop focuses on demonstrating the applicability of Formal Methods on modern complex systems with a high degree of self-adaptivity and reconfigurability, by bringing together researchers and practitioners with the goal of pushing forward the state of the art on logics and model checking.

cs.LO↗

arXiv2014

An LTL Semantics of Business Workflows with Recovery

We describe a business workflow case study with abnormal behavior management (i.e. recovery) and demonstrate how temporal logics and model checking can provide a methodology to iteratively revise the design and obtain a correct-by construction system. To do so we define a formal semantics by giving a compilation of generic workflow patterns into LTL and we use the bound model checker Zot to prove specific properties and requirements validity. The working assumption is that such a lightweight approach would easily fit into processes that are already in place without the need for a radical change of procedures, tools and people's attitudes. The complexity of formalisms and invasiveness of methods have been demonstrated to be one of the major drawback and obstacle for deployment of formal engineering techniques into mundane projects.

cs.SE↗

arXiv2014

On Formalisms for Dynamic Reconfiguration of Dependable Systems

Three formalisms of different kinds - VDM, Maude, and basic CCSdp - are evaluated for their suitability for the modelling and verification of dynamic software reconfiguration using as a case study the dynamic reconfiguration of a simple office workflow for order processing. The research is ongoing, and initial results are reported.

cs.SE↗

arXiv2013

Towards a Formalism-Based Toolkit for Automotive Applications

The success of a number of projects has been shown to be significantly improved by the use of a formalism. However, there remains an open issue: to what extent can a development process based on a singular formal notation and method succeed. The majority of approaches demonstrate a low level of flexibility by attempting to use a single notation to express all of the different aspects encountered in software development. Often, these approaches leave a number of scalability issues open. We prefer a more eclectic approach. In our experience, the use of a formalism-based toolkit with adequate notations for each development phase is a viable solution. Following this principle, any specific notation is used only where and when it is really suitable and not necessarily over the entire software lifecycle. The approach explored in this article is perhaps slowly emerging in practice - we hope to accelerate its adoption. However, the major challenge is still finding the best way to instantiate it for each specific application scenario. In this work, we describe a development process and method for automotive applications which consists of five phases. The process recognizes the need for having adequate (and tailored) notations (Problem Frames, Requirements State Machine Language, and Event-B) for each development phase as well as direct traceability between the documents produced during each phase. This allows for a stepwise verification/validation of the system under development. The ideas for the formal development method have evolved over two significant case studies carried out in the DEPLOY project.

cs.SE↗

arXiv2013

Issues about the Adoption of Formal Methods for Dependable Composition of Web Services

Web Services provide interoperable mechanisms for describing, locating and invoking services over the Internet; composition further enables to build complex services out of simpler ones for complex B2B applications. While current studies on these topics are mostly focused - from the technical viewpoint - on standards and protocols, this paper investigates the adoption of formal methods, especially for composition. We logically classify and analyze three different (but interconnected) kinds of important issues towards this goal, namely foundations, verification and extensions. The aim of this work is to individuate the proper questions on the adoption of formal methods for dependable composition of Web Services, not necessarily to find the optimal answers. Nevertheless, we still try to propose some tentative answers based on our proposal for a composition calculus, which we hope can animate a proper discussion.

cs.SE↗

arXiv2013

Social Networks and Collective Intelligence: A Return to the Agora

Nowadays, acquisition of trustable information is increasingly important in both professional and private contexts. However, establishing what information is trustable and what is not, is a very challenging task. For example, how can information quality be reliably assessed? How can sources? credibility be fairly assessed? How can gatekeeping processes be found trustworthy when filtering out news and deciding ranking and priorities of traditional media? An Internet-based solution to a human-based ancient issue is being studied, and it is called Polidoxa, from Greek "poly", meaning "many" or "several" and "doxa", meaning "common belief" or "popular opinion". This old problem will be solved by means of ancient philosophies and processes with truly modern tools and technologies. This is why this work required a collaborative and interdisciplinary joint effort from researchers with very different backgrounds and institutes with significantly different agendas. Polidoxa aims at offering: 1) a trust-based search engine algorithm, which exploits stigmergic behaviours of users? network, 2) a trust-based social network, where the notion of trust derives from network activity and 3) a holonic system for bottom-up self-protection and social privacy. By presenting the Polidoxa solution, this work also describes the current state of traditional media as well as newer ones, providing an accurate analysis of major search engines such as Google and social network (e.g., Facebook). The advantages that Polidoxa offers, compared to these, are also clearly detailed and motivated. Finally, a Twitter application (Polidoxa@twitter) which enables experimentation of basic Polidoxa principles is presented.

cs.SI↗

arXiv2012

On Methods for the Formal Specification of Fault Tolerant Systems

This paper introduces different views for understanding problems and faults with the goal of defining a method for the formal specification of systems. The idea of Layered Fault Tolerant Specification (LFTS) is proposed to make the method extensible to fault tolerant systems. The principle is layering the specification in different levels, the first one for the normal behavior and the others for the abnormal. The abnormal behavior is described in terms of an Error Injector (EI), which represents a model of the erroneous interference coming from the environment. This structure has been inspired by the notion of idealized fault tolerant component but the combination of LFTS and EI using Rely/Guarantee reasoning to describe their interaction can be considered as a novel contribution. The progress toward this method and this way to organize fault tolerant specifications has been made experimenting on case studies and an example is presented.

cs.SE↗

arXiv2010

Design of QoS-aware Provisioning Systems

We present an architecture of a hosting system consisting of a set of hosted Web Services subject to QoS constraints, and a certain number of servers used to run users demand. The traffic is session-based, while provider and users agree on SLAs specifying the expected level of service performance such that the service provider is liable to compensate his/her customers if the level of performance is not satisfactory. The system is driven by a utility function which tries to optimize the average earned revenue per unit time. The middleware collects demand and performance statistics, and estimates traffic parameters in order to make dynamic decisions concerning server allocation and admission control. We empirically evaluate the effects of admission policies, resource allocation and service differentiation schemes on the achieved revenues, and we find that our system is robust enough to successfully deal with session-based traffic under different conditions.

cs.NI↗

arXiv2010

Deriving Specifications of Dependable Systems: toward a Method

This paper proposes a method for deriving formal specifications of systems. To accomplish this task we pass through a non trivial number of steps, concepts and tools where the first one, the most important, is the concept of method itself, since we realized that computer science has a proliferation of languages but very few methods. We also propose the idea of Layered Fault Tolerant Specification (LFTS) to make the method extensible to dependable systems. The principle is layering the specification, for the sake of clarity, in (at least) two different levels, the first one for the normal behavior and the others (if more than one) for the abnormal. The abnormal behavior is described in terms of an Error Injector (EI) which represents a model of the erroneous interference coming from the environment. This structure has been inspired by the notion of idealized fault tolerant component but the combination of LFTS and EI using rely guarantee thinking to describe interference can be considered one of the main contributions of this work. The progress toward this method and the way to layer specifications has been made experimenting on the Transportation and the Automotive Case Studies of the DEPLOY project.

cs.SE↗

arXiv2010

On Modelling and Analysis of Dynamic Reconfiguration of Dependable Real-Time Systems

This paper motivates the need for a formalism for the modelling and analysis of dynamic reconfiguration of dependable real-time systems. We present requirements that the formalism must meet, and use these to evaluate well established formalisms and two process algebras that we have been developing, namely, Webpi and CCSdp. A simple case study is developed to illustrate the modelling power of these two formalisms. The paper shows how Webpi and CCSdp represent a significant step forward in modelling adaptive and dependable real-time systems.

cs.SE↗