Predicting behavior and assuring quality of service of complex multimedia systems is very hard. Techniques based on tests, inspections or simulations are not always effective. Conversely, rigorous adoption of formal approaches in entire system lifecycle is very costly, and does not provide evidence about run-time performance. Our research proposes a tool, which allows both formally modeling and simulating a Mobile Ad-hoc NETwork - MANET. Previous paper of same authors discussed the tool effectiveness in simulating the system; the present paper deals with the Petri Nets-based model of MANET behavior, and shows the model usefulness in predicting some interesting computational properties.

Grid systems technology has evolved over recent years and the Open Grid Service Architecture (OGSA) has rapidly become the “de facto” standard. OGSA includes several important capabilities needed to support Grid applications and, among them, the job management and execution capability, which concern searching candidate locations and executing and managing jobs until end. Such functionalities enable users to use distributed resources for their applications. These tasks are critical in the Grid system context because their incorrect execution can heavily affect provided services, so adoption of formal method is sometimes mandatory. This paper is aimed at defining an abstract model for specifying the job management and execution services. We propose a Distributed Abstract State Machine (DASM) model

n this paper, we investigate the user's reactions to received suggestion by an Embodied Conversational Agent playing the role of artificial therapist in the healthy eating domain. Specifically, we analyse the behaviour of people who voluntarily requested to receive information from the agent, and we compare it with the results of a previous evaluation experiment in which subjects were not properly motivated to interact with the agent because they were selected for evaluating the system. This study is part of an ongoing research aimed at developing an intelligent virtual agent that applies natural argumentation techniques to persuade the users to improve their eating habits.

Several problems related to communication among Mobile Ad-hoc NETworks (MANETs) devices can be faced making use of formal models. Among these, Petri Nets are particularly suitable for modeling dynamic and transitional systems. The tool DEMONE models the behavior of each host in a MANET through a Petri Nets extension, so that it allows the analysis of some interesting computational activities and the study of performance of the modeled MANET

Job Execution Management Services in Grid systems are generally implemented using specific Grid middleware, and they are considered very critical for the success of the entire system. In order to better manage complexity and criticality, literature suggests the use of robust formal models to describe and analyze these services. This paper abstracts strategic services in Grid Systems, proposes an Abstract State Machine-based model to design them, and implements them by the coreASM tool. The obtained results lead to consider the usage of Abstract State Machine models as a concrete control appliance for Grid systems

Mobile Ad-hoc NETworks (MANETs) are wireless networks designed for communications among nomadic hosts in absence of fixed infrastructure. Different reactive protocols for MANETs, in which routes are established only when needed, provide different network topology awareness (NTA) to each host, depending on their algorithmic features. NACK-based AODV (N-AODV) is a variant of the well-known Ad-hoc On-demand Distance Vector (AODV) reactive protocol for MANETs we proposed with the aim of improving NTA of the original protocol. In this paper, a performance comparison between AODV and N-AODV is conducted in order to investigate whether N-AODV effectively improves NTA with respect to AODV, and how this improvement affects both its effectiveness and efficiency. The experiment is executed within a simulation environment. The obtained results show that a MANET adopting N-AODV exploits higher NTA than a MANET adopting AODV. Moreover, the improved awareness impacts effectiveness and efficiency of routing activities because, in the long-run, it results in a lower need to activate the route discovery process for establishing new communications sessions.

Network topology awareness (NTA) is a fundamental issue in the context of computer networks: the lack of control over the topology can negatively impact performance, security, resilience, and so on. However, in Mobile Ad-hoc NETworks (MANETs), NTA is difficult to achieve because of their dynamicity. Different reactive protocols for MANETs, in which routes are established only when needed, provide different NTA to each host, depending on their algorithmic features. NACK-based AODV (N-AODV) is a variant of the well-known Ad-hoc On-demand Distance Vector (AODV) reactive protocol for MANETs which we proposed with the aim of improving the NTA of the original protocol. In this paper, an experiment aimed at comparing N-AODV to AODV is reported; it moves from an exploratory case study we conducted preliminarily. The results obtained show that a MANET adopting N-AODV exploits higher NTA than a MANET adopting AODV. Moreover, the improved awareness positively impacts effectiveness.

In this paper we present CoRSAR, a mobile recommender system for the tourism domain in Augmented Reality. It allows the users to explore and visit a city and provides recommendation of Point of Interests (POIs) by combining collaborative filtering and context-awareness. In this paper, besides describing the system, we present the results of a study aiming at evaluating if users were more satisfied with the system recommendations when context features were taken into account. Results show that users provided a better evaluation of the system when the context-aware approach was adopted rather then the simple collaborative filtering one.

The inherent features of Mobile Ad-hoc NETworks (MANETs) make them vulnerable to various kinds of security attacks. In particular, in a so-called blackhole attack, one or more malicious hosts can send fake routing information towards an initiator, compromising the reliability of the network in the whole. In this paper, we propose a refinement of the NACK-based Ad-hoc On-demand Distance Vector (N-AODV) protocol, namely Blackhole-free N-AODV (BNAODV), as a solution to intercept (cooperative) blackhole attacks in MANETs. Thanks to a formalization through an Abstract State Machine-based model, the correctness of the proposed protocol is formally proved.

Abstract State Machines (ASMs) are very helpful in analyzing critical and complex systems, but they lack of inherent, domain-independent characterizations of computationally interesting properties. Our long-term research aims at providing an ASM-based characterization of the starvation-freedom property. To this end, in the present paper the Ad-hoc On-demand Distance Vector (AODV) routing protocol for Mobile Ad-hoc NETworks (MANETs) is modeled through ASMs, and starvation is studied. This experience suggests us to focus on vulnerable rules as the key issue that drives the risk of starvation within the ASM framework.

Several problems related to communication among Mobile Ad-hoc NETworks (MANETs) devices can be faced making use of formal models. Among these, Petri Nets are particularly suitable for modeling dynamic and transitional systems. The tool DEMONE models the behavior of each host in a MANET through a Petri Nets extension, so that it allows the analysis of some interesting computational activities and the study of performance of the modeled MANET

Several formalisms have been applied for addressing development issues in Mobile Ad-hoc NETworks (MANETs), however they usually lack of understandability, expressiveness and executability features. Instead, the Abstract State Machine (ASM) formalism does not suffer these limitations and can provide a useful conceptual tool for reasoning about MANET behavior. This paper shows the practical suitability of ASMs in capturing the specific MANET issues: concurrency, communications, and so on. To this end, the Ad-hoc On-demand Distance Vector (AODV) routing protocol for MANETs is modeled, and some properties of interest are proved.

Ambient Intelligence solutions may provide a great opportunity, for elder people, to live longer at home. When assistance and care are delegated to the intelligence embedded in the environment, besides considering task-oriented response to the user needs, it is necessary to take into account the establishment of social relations. To this aim, it becomes crucial to model both the rational and the affective components of the user state of mind. In this chapter we will mainly focus on the problem of modeling the cognitive and affective variables involved in the definition of a user model suitable for this domain. After provid-ing an overlook of the state of the art, we report about our experience in designing NICA (as the name of the project Natural Interaction with a Caring Agent), a social agent acting as a virtual caregiver able to assist elderly people in a smart environment for taking care of both the physical and mental state of the users.