This paper proposes a method for formally modeling and analyzing mutual exclusion algorithms. The process starts with Uppaal timed automata and model checking. A Uppaal model is then reduced to a Java actor program to overcome the scalability issues associated with exhaustive verification. The method is applied to mutual exclusion in anonymous shared memory (ASM). ASM is challenging because concurrent/parallel processes do not agree on the names of the shared registers. Rather, each process uses a permutation of the register names. Processes have unknown identifiers and are symmetric, that is, they execute the same code. ASM is natural in bio-inspired, molecular applications. As a case study, the paper investigates a recent ASM mutual exclusion solution proposed by Taubenfeld. The algorithm proves correct for N=2 processes when m≥7 (m odd) registers are used. The algorithm does not extend to N≥3 processes. As a new contribution, this paper develops and formalizes a solution (TT - T2) that embeds Taubenfeld's algorithm for 2 processes (T2) in a tournament binary tree (TT) organization, where the basic algorithm acts as the arbitration unit in TT nodes. The paper demonstrates, through simulations of the reduced and scalable actor program, that the TT - T2 represents an effective solution for mutual exclusion in ASM for N≥2 processes.

This paper proposes an algorithm, named HWK-Sets, based on K-Means, suited for clustering data which are variable-sized sets of elementary items. Clustering sets is difficult because data objects do not have numerical attributes and it is not possible to use the classical Euclidean distance upon which K-Means is normally based. An adaptation of the Jaccard distance between sets is used, which exploits application-sensitive information. More in particular, the Hartigan and Wong variation of K-Means is adopted which uses medoids as cluster representatives, can work with several seeding methods and can favor the fast attainment of a careful solution. The paper introduces HWK-Sets which is implemented in Java by parallel streams. Then, the efficiency and accuracy of HWK-Sets are demonstrated by simulation experiments.

This paper proposes a variation of the K-Means clustering algorithm, named Population-Based K-Means (PBK-MEANS), which founds its behaviour on careful seeding. The new K-Means algorithm rests on a greedy version of the K-Means++ seeding procedure (g_kmeans++), which proves effective in the search for an accurate clustering solution. PB-K-MEANS first builds a population of candidate solutions by independent runs of K-Means with g_kmeans++. Then the reservoir is used for recombining the stored solutions by Repeated K-Means toward the attainment of a final solution which minimizes the distortion index. PB-KMEANS is currently implemented in Java through parallel streams and lambda expressions. The paper first recalls basic concepts of clustering and of K-Means together with the role of the seeding procedure, then it goes on by describing basic design and implementation issues of PB-K-MEANS. After that, simulation experiments carried out both on synthetic and real-world datasets are reported, confirming good execution performance and careful clustering.

Solving large-scale clustering problems requires an efficient algorithm which can be implemented also in parallel. K-means would be suitable but it can lead to an inaccurate clustering result. To overcome this problem, we present a parallel version of random swap clustering algorithm. It combines the scalability of k-means with high clustering accuracy. The new clustering method is experimented on top of Java parallel streams and lambda expressions, which offer interesting execution time benefits. The method is applied to standard benchmark datasets, with a varying population size and distribution of managed records, dimensionality of data points and the number of clusters. The experimental results confirm that high quality clustering can be obtained by parallel random swap together with a high time efficiency.

The work described in this paper develops a methodology for modelling and analysis of complex timed systems. The methodology is based on the Stochastic Reward Nets (SRN) [1]–[4] formalism, which has gained its popularity by its ability to enable the studying of the performability, reliability and availability of, e.g., computer and communication systems. SRN is an extension of Generalized Stochastic Petri Nets (GSPN) and it is supported by such tools as the Stochastic Petri Net Package (SPNP) [5]–[6]. Power and accuracy in the application of SRN derive from mapping a model into a corresponding Markov Reward Model (MRM) from which quantitative measures are extracted in terms of reward functions associated to tangible markings of the source model. To cope with large models which cause state explosions in the underlying MRM, simulations are used [2].

The following topics are dealt with: cloud computing; Internet of Things; autonomous aerial vehicles; learning (artificial intelligence); parallel processing; virtualisation; formal verification; distributed processing; computer simulation; scheduling.

Home Energy Management Systems (HEMSs) are devoted to monitoring and control the operation of domestic appliances in order to purposely shape the in-home energy consumption curves. A challenge in the design and implementation of a HEMS is to guarantee a proper coupling between the cyber discrete part of the system with the continuous modes of the physical environment in which the HEMS operates. This paper is concerned with the development of a HEMS by using the Theatre actor system. Theatre favors the construction of cyber-physical systems (CPSs) by exploiting a notion of hybrid actors. As a key feature, Theatre enables a same actor model to be exploited during the analysis, design, prototyping and implementation phases of a CPS. For analysis purposes, a Theatre model is reduced to UPPAAL hybrid timed automata for property assessment by statistical model checking.

This paper describes a formal approach to modelling and verification of self-adaptive real-time systems. Such systems can dynamically be affected by exception events either originated in the operational environment or in the internal status, which require to be dealt with through adaptation actions which have to fulfil timing constraints. The approach is based on Time Basic (TB) Petri nets, a formalism well-suited to the specification of time-critical systems. Although some specialcase tools have been developed to support the analysis of TB net models, the original contribution of this paper is an embedding of TB nets into the popular Uppaal toolbox based on timed automata, which makes it possible both non-deterministic exhaustive analysis by model checking and/or a quantitative analysis of model properties through statistical model checking. The paper demonstrates the application of TB net modelling and analysis through a self-healing time-critical system.

Theatre is a control-based, light-weight, reflective actor system designed to address the development of general distributed, timed (possibly probabilistic) systems and cyber-physical systems in particular. Theatre is characterized by its formal operational semantics. An abstract Theatre model, including the services of a possible deterministic network and associated protocol, can be analyzed by exhaustive model-checking or by statistical model checking or through ad-hoc simulators. Theatre is currently implemented in Java. Other languages are possible. A key point of Theatre is its volition to favoring a seamless transformation of an analyzed model into the terms of design and implementation phases. The tutorial will illustrate the modelling aspects of Theatre, its supporting analysis tools, its capability of combining discrete-time with continuous time, its maturity as a software engineering methodology, and some developed applications.

This paper describes a modelling and analysis experience concerning time synchronization in wireless sensor networks (WSN). A fully distributed algorithm is formally modelled and its properties assessed through statistical model checking. The described work is based on the Theatre framework which rests on actors and asynchronous message passing. Theatre can be reduced to the Uppaal Statistical Model Checker (SMC). The paper discusses the chosen time synchronization algorithm, outlines the Theatre modelling features and its mapping on to Uppaal Smc, and shows a Theatre model for the selected time synchronization algorithm enhanced with a new adaptation mechanism for energy saving. The model is then analyzed through simulations.

This paper proposes an approach to modelling and analysis of distributed real-time actor systems, which is based on the Uppaal statistical model checker (SMC). SMC was chosen because it automatizes simulations, offers a temporal logic language to formalize specifications and exploits statistical techniques to infer quantitative measures about a model. The approach is integrated in a system life-cycle where a same model can be transitioned without distortions from analysis down to design and implementation, currently based on Java. The paper describes the adopted actor modelling language and its architectural framework, illustrates the Uppaal SMC approach and demonstrates its practical usefulness through a running example.

This paper proposes modelling and exhaustive verification of mutual exclusion algorithms using timed automata (TA) and the popular UPPAAL toolbox. The proposal allows to check all the properties of a mutual exclusion algorithm also along the time dimension. Both the classic case of atomic read/write operations on memory cells and the non determinism of reading a memory cell during one or multiple write operations on it as it may occur in modern multi-port memories are considered. The approach is then applied to some algorithms proposed in the literature of which known properties are confirmed but also new ones are revealed.

The development of Cyber-Physical Systems (CPSs) is challenging because the cyber part (software) has to control, through sensors/actuators accessed by means of a suitable network infrastructure, a physical plant which can require the fulfillment of timing constraints. This paper proposes a methodology based on a control-centric agent framework, for the development of CPSs. The approach is original and enables model continuity, i.e., the same model can be exploited along all the development stages of a system, from analysis based on simulation down to real-time implementation and execution. For demonstration purposes, a case study concerned with optimizing power management in an electric power grid is reported.

Summary This work centres on a control framework for general multi‐agent systems, which separates the design of agents behaviours (the application layer) from crosscutting control concerns (the control layer) regulating message exchange and processing. The goal is to support modelling and execution of a multi‐agent system whose evolution is transparently governed by a pluggable control structure. A library of different control structures, including pure‐concurrent and time‐sensitive (real‐time and simulation) strategies, was developed. The paper describes the developed control framework and focusses on the achievement of control strategies compliant with agent mobility and resource availability. The control design rests on a minimal actor computational model extended with actions, which are independent computational tasks able to execute in parallel. The approach enablesmodel continuity, that is, the same model is used from analysis by simulation to implementation and real‐time execution. The framework is prototyped on top of the JADE agent infrastructure. Usability and effectiveness of the resultant approach are demonstrated by a case study based on a complex closed queue network of services. On‐going and future work is finally pointed out in the conclusions. Copyright © 2016 John Wiley & Sons, Ltd.

This paper proposes an original framework for modelling and verification (M&V) of starvation-free mutual exclusion algorithms based on weak semaphores, that are without a built-in waiting-process queue.The goal is to support the implementation of light-weight starvation-free semaphores useful in general concurrent systems including cyber physical systems.The M&V approach depends on UPPAAL.First known weak semaphores are modelled.Then they are exploited for model checking classic algorithms.Known properties are retrieved but subtle new ones are discovered.As part of the developed approach, a new algorithm is proposed which uses two semaphores of the weakest type, N bits (N being the number of processes) and a counter.This algorithm too is proved to be correct.

Time Petri Nets (TPN) are a well-known formalism for modelling time-dependent systems with timing constraints.This paper proposes an approach based on a stochastic extension of TPN (sTPN), which enables both qualitative assessment of feasible temporal behaviors through model checking, and quantitative evaluation of a probability measure of a given behavior, by statistical model checking.The experimental work rests on the use of the latest version of the UPPAAL toolbox which supports both exhaustive non deterministic analysis and statistical model checking of system properties.The approach is demonstrated through an example.

Generalized Stochastic Petri Nets (GSPN) are a well-known timed extension of Petri nets suited for modelling and performance analysis of general time-dependent concurrent systems. The work described in this paper develops an original structural translation of GSPN models onto UPPAAL SMC so as to enable property estimation through statistical model checking. The actual GSPN supported formal language admits, in general, tagged tokens carrying timestamps, queuing places, normal, transport and inhibitor arcs and timed and untimed transitions. This paper describes the proposed approach and demonstrates its practical usefulness through a case study.

Summary Multi‐agent systems have been proven very effective for the modelling and simulation (M&S) of complex systems like those related to biology, engineering, social sciences and so forth. The intrinsic spatial character of many such systems leads to the definition of a situated agent. A situated agent owns spatial coordinates and acts and interacts with its peers in a hosting territory. In the context of parallel/distributed simulation of situated agent models, the territory represents a huge shared variable that requires careful handling. Frequent access by agents to territory information easily becomes a bottleneck degrading system performance and scalability. This paper proposes an original approach to modelling and distributed simulation of large‐scale situated multi‐agent systems. Time management is exploited for resolving conflicts and achieving data consistency while accessing the environment. The approach allows a simplification of the M&S tasks by making the modeller unaware of distribution concerns while ensuring the achievement of good scalability and performance during the distributed simulation. Practical aspects of the approach are demonstrated through some modelling examples based on Tileworld. Copyright © 2014 John Wiley & Sons, Ltd.

This paper proposes a control framework for modelling and executing parallel/distributed multi-agent systems. The goal is to clearly separate agent behaviours (the application layer) from crosscutting control concerns (the control layer) which in general are orthogonal to a specific application and transparently affect and regulate its evolution. Different control strategies, ranging from pure concurrent to time sensitive (real-time or simulation) can be considered and applied as a plug-in to a multi-agent system. In this work the control framework is tailored to the JADE agent infrastructure, using a minimal actor computational model. JADE was chosen because it is widely used and open source, it adheres to FIPA communication standards which in turn favour application interoperability, it is based on Java. JADE, however, lacks of any built-in solution for developing time sensitive applications. This paper describes the proposed control framework in JADE and focusses on the achievement of control strategies compliant with agent mobility and resource availability. All of this favours model continuity, i.e. a seamless transformation from model analysis by simulation to model implementation and real time execution. A case study concerning a closed queue network is used for demonstrating the practical aspects of the approach. Finally, an indication of on-going and future work is provided in the conclusions.

This paper proposes an agent-based control framework in JADE which allows the construction of control extensions tailored to the application needs. The approach is based on a minimal actor model which simplifies JADE agent programming. A catalog of reusable control forms, both concurrent/parallel and time-dependent (real time or simulation time are supported) was achieved. The paper introduces the control framework, clarifies its implementation status and demonstrates its practical use

Repast Simphony (RS) is a popular toolbox for agentbased modeling and simulation (ABMS) of complex systems. It can be used from within the Eclipse IDE with Java being the main implementation language. Moreover, visual modeling is supported by agent flowcharts. Powerful features of RS include contexts and projections which allow the modeler to build e.g. situated multi-agent systems (MAS) which can easily be configured and visualized in the RS runtime system. RS lacks of a reference agent methodology. Rather the modeler is free to define and follow her/his own methodology with RS: procedurally, declaratively or visual-based. This openness was exploited in this work for supporting different notions of agents, thus addressing the modeling needs of various application domains. In particular this paper proposes an embed in RS of an actor model which provides a lightweight notion of agents. The actor model is then used as a kernel for supporting more abstract but rigorous modeling languages like Parallel DEVS (P−DEVS) and time-extended Petri nets. A P−DEVS modeling example is reported to demonstrate the usefulness of supporting multiple agent methodological layers in RS.

The work presented in this paper concerns the development of a smartphone application for the monitoring of energy consumption relative to a domestic electricity grid. An algorithm has been integrated in the smartphone application allowing Enel (the main Italian Electrical Company) customers to have, on their mobile phone, clear and transparent information about the energy consumption of their houses in real time.

This paper proposes an original schedulability framework which is based on preemptive Time Petri Nets (pTPNs) and UPPAAL with stopwatches (UPPAALSW). The realization enables a real-time tasking set, along with precedence constraints in the form of data control, message passing etc., to be uniformly formalized using pTPNs and then analyzed through model checking using UPPAALSW in the presence of a reusable library of template processes modelling transitions of the source pTPNs specification and the scheduler algorithm which can be based on fixed priority or earliest deadline first. The paper first introduces and motivates the proposed approach by relating it to similar work described in literature, then summarizes the pTPNs formalism through a modelling example. After that the prototyped library in UPPAALSW is presented and put to work for model checking the chosen real-time tasking set. Analysis of models which depend e.g. on non deterministic execution times and sporadic arrival times of tasks, is conditioned by the use of an over approximation in the generation of the model state graph.

This paper describes an experience of porting the THEATRE agent architecture on top of the grid. The agent architecture consists of light-weight actors and computational theatres which have been proven to be well suited for modeling and simulation of complex systems. THEATRE nodes act as agencies that provide common services of message scheduling and dispatching to mobile actors. THEATRE is currently implemented in Java and can work with different transport layers and middleware. In the last years it was successfully interfaced to HLA/RTI, Terracotta, Java Sockets and Java RMI. The work described in this paper aims at experimenting with THEATRE over the grid, using in particular the Globus toolkit. The goal is to open THEATRE to the exploitation of virtual organizations of computing resources with secure communications, and to favor simulation interoperability through grid services. The paper summarizes THEATRE, describes a design and prototype implementation of THEATRE on top of the Globus Toolkit 4 (GT4), and demonstrates its practical use by means of a modeling example.

This work develops techniques for modeling and distributed simulation of complex situated multi-agent systems, which are highly dynamic and possess an intrinsic spatial character. Each agent owns its spatial coordinates and acts and interacts with its peers in a hosting territory. In a distributed/parallel scenario of a typical situated agent model, the territory represents a huge shared variable. Frequent access by agents to territory information easily becomes a bottleneck degrading system performance and scalability. This paper proposes an original approach and supporting API to distributing situated multi-agent models using actors. The approach exploits time management for resolving conflicts and to achieve data consistency. Approach contribution is twofold: (a) it simplifies M&S tasks by making the modeler unaware of distribution concerns, (b) it is capable of ensuring good model scalability and simulation performance. Practical aspects of the approach are demonstrated by a Tile-World model and its distributed simulation experiments.

The minority game (MG) is a simple yet effective binary-decision model which is well suited to study the collec-tive emerging behaviour in a population of agents with bounded and inductive rationality when they have to compete, through adaptation, for scarce resources. The original formulation of the MG was inspired by the W.B. Arthur’s El Farol Bar problem in which a fixed num-ber of people have to independently decide each week whether to go to a bar having a limited capacity. A de-cision is only affected by information on the number of visitors who attended the bar in the past weeks. In its basic version, the MG does not contemplate communi-cation among players and it supposes that information about the past game outcomes is publicly available. This paper proposes the Dynamic Sociality Minority Game (DSMG), an original variant of the classic MG where (i) information about the outcome of the previously played game step is assumed to be known only by the agents that really attended the bar the previous week and (ii) a dynamically established acquaintance relationship is in-troduced to propagate such information among non at-tendant players. Particular game settings are identified which make DSMG able to exhibits a better coordina-tion level among players with respect to standard MG. Behavioral properties of the DSMG are thoroughly an-alyzed through an agent-based simulation of a simple road-traffic model.

synchronizers, timed automata, UPPAAL, Java. This paper describes the design and implementation of a library of reusable UPPAAL template processes which support reasoning and property checking of concurrent programs, e.g. to be realized in the Java programming language. The stimulus to the development of the library originated in the context of a systems programming undergraduate course. The library, though, can be of help to general practitioners of concurrent programming which nowadays are challenged to exploiting the potentials of modern multi-core architectures. The paper describes the library and demonstrates its usage to modelling and exhaustive verification of mutual exclusion and common concurrent structures and synchronizers. UPPAAL was chosen because it is a popular and continually improved toolbox based on timed automata and model checking and it is provided of a user-friendly graphical interface which proves very important for debugging and property assessment of concurrent models. Java was considered as target implementation language because of its diffusion among application developers.

This paper describes a novel approach to parallel simulation of complex multi-agent systems which is based on actors and the Java middleware Terracotta. The approach aims to an exploitation of the computing power of modern multicore machines. Terracotta was chosen because it transparently allows to cluster the JVM. The paper discusses design and implementation aspects of the approach, and demonstrates the achievable execution performance through the parallel simulation of a scalable multi-agent system based on the predator/prey model.

This paper reports about a research project-HLA ACTOR REPAST- aimed to distributing RePast models thus potentially corresponding to the computational demands of large and reconfigurable multi-agent systems (MASs). Novel in HLA ACTOR REPAST is an exploitation of a lean actor infrastructure implemented in Java. Actors bring to RePast agents such features as migration, location-transparent naming,efficient communications, and a control-centric framework.Actors can be orchestrated by an in-the-large custom control structure which can ensure the necessary message causality constraints. Distribution and time management concerns depend on the IEEE standard HLA middleware. The paper first discusses details of the software engineering process underlying HLA ACTOR REPAST. The mapping techniques, based on Java text annotations and aspect oriented programming, minimize¿code intrusions¿ in the original model. Then the paper describes some experiments and performance results of applying HLA ACTOR REPAST to a distributed version of a RePast Tileworld model.

RePast is a well-known agent-based toolkit for modelling and simulation of complex systems. The toolkit is normally used on a single workstation, where modelling, execution and visualization aspects are dealt with. This paper describes an approach aimed to distributing RePast models, with minimal changes, over a networked context so as to address very large and reconfigurable models whose computational needs (in space and time) can be difficult to satisfy on a single machine. Novel in the approach is an exploitation of a lean actor infrastructure implemented in Java. Actors bring to RePast agents migration, location-transparent naming, efficient communications, and a control-centric framework. Actors can be orchestrated by an in-thelarge custom control structure which can ensure the necessary message precedence constraints. Preliminary experience is being carried out using HLA/RTI as middleware. However, the realization can also work with other standard transport layers such as Java Socket and Java RMI. The paper introduces the design rationale behind mapping RePast on to actors and discusses a distributed example.

This paper discusses the use of Theatre, a multi-agent simulation architecture, for the distributed simulation of discrete event systems (DESs) whose entities express complex behaviours. Complexity is dealt with by exploiting statechart-based actors which constitute the basic building blocks of a model. Actors are lightweight reactive autonomous agents that communicate to one another by asynchronous message passing. The threadless character of actors saves memory space and fosters efficient execution. The behaviour of actors is specified through “distilled statecharts” that enable hierarchical and modular specifications. Distributed simulation is accomplished by partitioning the system model among a set of logical processes (theatres). Timing management and intertheatre communications rest on High Level Architecture (HLA) services. The paper highlights the current implementation status and demonstrates the practical application of the approach through a manufacturing system model.

Hierarchical communicating real-time state machines (H-CRSM) is a formal modelling language for the modular development of distributed real-time systems. The formalism is characterized by the use of state transitions with guarded commands and timing constraints, the adoption of a few distilled statecharts constructs, and the modular specification of timing constraints along a state hierarchy. This paper proposes a translation of H-CRSM into UPPAAL which enables model checking. Translation rests on unfolding a hierarchical model on a flat representation

The paper describes a methodology for the development of real time systems and shows its application to the modeling, analysis and implementation of distributed multimedia systems. The methodology is centered on Communicating Real-Time State Machines as the modeling language and is supported by jCRSM, a Java2 based toolset. The latter provides a graphical environment for editing, testing, debugging and Java code generation of a prototyped system. Multimedia systems are particular real time systems which normally do not have hard deadlines to fulfill but only soft deadlines concerning the achievement of a user-defined level of quality of service. For instance, timing QoS parameters refer to jitter, skew and end-to-end delay, which are to be kept bounded throughout a multimedia session. QoS constraints are monitored by assertions on the recorded timestamped event histories. The paper reports some experimental results of a modeled remote multimedia presentation system.