Indoor environments are increasingly exposed to natural hazards, posing significant challenges for ensuring both preparedness and effective emergency response. However, existing monitoring solutions typically address either routine environmental control or post-event analysis, lacking mechanisms for dynamic reconfiguration across operational conditions. This paper presents a distributed IoT system for indoor disaster preparedness and response, grounded in an operational framework that provides a unified rationale for analyzing and managing indoor living environments. The proposed system integrates environmental and structural sensing, edge-level event detection, and cloud coordination services to enable continuous monitoring under normal conditions and coordinated reconfiguration during emergencies. A dual-regime operational model distinguishes preparedness and response phases, enabling state transitions triggered by critical events. The system is evaluated through a six-month real-world deployment in an educational environment, which provides qualitative and quantitative evidence of its behavior under operational conditions, and through controlled laboratory tests to assess its dual-regime behavior. The results show that the proposed system supports operational awareness and the reconfiguration of coordinated behavior in indoor environments.

In recent years, spatio-temporal graph neural networks (GNNs) have attracted considerable interest in the field of time series analysis, due to their ability to capture, at once, dependencies among variables and across time points. The objective of this systematic literature review is hence to provide a comprehensive overview of the various modeling approaches and application domains of GNNs for time series classification and forecasting. A database search was conducted, and 366 papers were selected for a detailed examination of the current state-of-the-art in the field. This examination is intended to offer to the reader a comprehensive review of proposed models, links to related source code, available datasets, benchmark models, and fitting results. All this information is hoped to assist researchers in their studies. To the best of our knowledge, this is the first and broadest systematic literature review presenting a detailed comparison of results from current spatio-temporal GNN models applied to different domains. In its final part, this review discusses current limitations and challenges in the application of spatio-temporal GNNs, such as comparability, reproducibility, explainability, poor information capacity, and scalability. This paper is complemented by a GitHub repository at https://github.com/FlaGer99/SLR-Spatio-Temporal-GNN.git providing additional interactive tools to further explore the presented findings.

Blockchain technology has been widely adopted to enhance the security and the decentralisation of smart applications in large-scale pervasive systems. In such a context, data extraction is crucial as it provides a better understanding of the system’s behaviours. However, several challenges arise in automatically extracting data, due to the variety of data sources, such as transactions, events, contract storage, and the complexity of the blockchain structure. In particular, retrieving smart contract state changes remains unexplored despite its potential usage for discovering unexpected behaviour. For such reasons, in this work, we propose a novel methodology and a supporting application for extracting smart contract state changes and other execution-related data. The obtained data is then decoded and offered in a standard format to be easily reused. The methodology provides additional functionalities such as transaction filtering and capabilities for querying over extracted data. The effectiveness and the performance of the methodology were evaluated on three real-world projects from different EVM-based blockchains.

The recent growth of blockchain has opened the use of technology for supporting the creation of newkinds of trustable systems. Model-driven engineering methodologies have been conceived to facilitate the automatic generation and deployment of software applications starting from the definition and refinement of abstract specification. BPMN choreography diagrams permit the representation of inter-organisational systems from a high-level perspective, just focusing on message exchange. However, the usage of such models in a blockchain-based setting has been limited to scenarios in which parties are involved in single interactions. This aspect becomes significantly relevant when considering complex applications, particularly those in the realm of the Internet of Things. In these cases, the multiplicity of parties and their actions is crucial and requires novel solutions. In this work, we propose a novel approach for modelling, refining, deploying, and executing a choreography on the blockchain, taking into account those scenarios in which the model includes multiple instances. In particular, the considered models are translated into smart contracts able to correctly manage multiplicity. To demonstrate the approach’s feasibility, we designed and presented a smart thermostat application, which is executed on the Polygon blockchain.

The public blockchain lacks data confidentiality. Although a level of anonymity seems guaranteed, it is still possible to link transactions and disclose related information. A solution to the privacy problem is to use cryptography in transactions, however this can lead to increased costs and slowdown in network throughput. Recent works experiment with advanced cryptography, in particular Zero-Knowledge proofs (ZK-proofs) can be supplied within a transaction to prove its validity, without revealing sensitive information. We analyze solutions that adopt ZK-proofs, such as Confidential Transactions (CTs). Several challenges emerge depending on both the zero-knowledge system and the balance model considered (UTXO, hybrid or account model). For ZK-proofs, systems that do not introduce additional trust are required. On the other hand, the account model is the most flexible for addressing security challenges. Moreover, CTs do not fully exploit the potential of ZK-proofs, since each transaction comes with one or more ZK-proof for a single transfer. Within this paper, we present ZeroMT, a novel multi-transfer private payment scheme for account-based blockchains. Drawing inspiration from Zether, our approach extends their work to develop a payment model that supports multiple payees within a single transaction. This also benefits scalability: ZeroMT enriches the CTs with the aggregation property, i.e., the batch verification of multiple transfers from a single and aggregate proof. We show that in our extended model the overdraft-safety and privacy security properties still hold. We provide an implementation and evaluation of ZeroMT, which shows the benefits of aggregating multiple transfers.

In modern business scenarios, more and more organisations have to deal with the critical requirements of trustworthiness and flexibility, when collaborating in multi-party business processes. This calls for new kinds of systems able to manage collaborative processes in untrusted and dynamic environments. Concerning the collaborative perspective, the Business Process Management discipline has provided effective and standardised solutions for a long time, now. Regarding the trustworthiness perspective, blockchain is advocated as one of the most prominent technologies to guarantee trust in a multi-party setting. However, while the immutability of blockchain provides transparent and secure proof of past business interactions, it hinders the flexibility of the business process execution, as the business logic regulating the process execution is immutably stored in the blockchain. On the other hand, flexibility is a property that is becoming crucial in such a setting due to the high dynamism of the business scenarios. In fact, it permits to modify a process at run-time to deal with internal or external changes. In this paper, we face this issue by proposing an architecture for the flexible blockchain-based execution of multi-party business processes. In our approach, business processes are modelled by BPMN choreography diagrams translated into code, whose execution state is then stored in the blockchain. Flexibility is achieved by decoupling the business process’s logic from its execution state, thus allowing run-time changes to the process execution without losing the fundamental properties of trust provided by the blockchain. To show the effectiveness of our approach, we provide a prototypical implementation, called FlexChain, and we use it on a case study from the healthcare application domain. The results obtained by the analysis of cost for the reported case study show the feasibility of the approach. In particular, major costs to sustain relate to one-time operations, such as the deployment and the run-time update of the model, while the most frequent actions are quite efficient.

As a disruptive technology, the blockchain is continuously finding novel application contexts, bringing new opportunities and radical changes. In this paper, we use blockchain as a communication infrastructure to support multi-party business processes. In particular, through smart contracts specifically generated by the mentioned business process, it is possible to derive a trustable infrastructure enabling the interaction among parties. Moreover, the emergence of different blockchain technologies, satisfying different characteristics, gives the possibility to support the same business process dealing with different non-functional needs. In this paper, we propose a novel engineering methodology supported by a practical framework called Multi-Chain. It permits to derive, using a model-driven strategy, a blockchain-based infrastructure, that can be deployed over a specific blockchain technology (e.g., Ethereum or Hyperledger Fabric). The objective is to permit the single definition and multiple deployments of the business process, to deliver the same functionalities, but satisfying different non-functional needs. In such a way, organisations willing to cooperate can select the multi-party business process and the blockchain technology they would like to use to satisfy their needs. Using Multi-Chain, they will be able to automatically derive from a Business Process Modelling Notation (BPMN) choreography diagram a blockchain infrastructure ready to be used. This overcomes the need to get acquainted with many details of the specific technology.

The BPMN 2.0 standard is nowadays largely used to model distributed informative systems in both academic and industrial contexts. The notation makes possible to represent these systems from different perspectives. A local perspective, using collaboration diagrams, to describe the internal behaviour of each component of the systems, and a global perspective, using choreography diagrams, where the interactions between system components are highlighted without exposing their internal structure. In this paper, we propose a formal approach for checking conformance of collaborations, representing possible system implementations, with respect to choreographies, representing global constraints concerning components' interactions. In particular, we provide a direct formal operational semantics for both BPMN collaboration and choreography diagrams, and we formalise the conformance concept by means of two relations defined on top of the semantics. To support the approach into practice we have developed the C 4 tool. Its main characteristic is to make the exploited formal methods transparent to systems designers, thus fostering a wider adoption of them in the development of distributed informative systems. We illustrate the benefits of our approach by means of a simple, yet realistic, example concerning a traveling scenario.

Intelligent Environments (IE) are a very active area of research and a number of applications are currently being deployed in domains ranging from smart home to e-health and autonomous vehicles. In a number of cases, IE operate together with (or to support) humans, and it is therefore fundamental that IE are thoroughly verified. In this paper we present how a set of techniques and tools developed for the verification of software code can be employed in the verification of IE described by means of event-condition-action rules. In particular, we reduce the problem of verifying key properties of these rules to satisfiability and termination problems that can be addressed using state-of-the-art SMT solvers and program analysers. We introduce a tool called vIRONy that implements these techniques and we validate our approach against a number of case studies from the literature.

Business Process Modelling has acquired increasing relevance in software development. Available notations, such as BPMN, permit to describe activities of complex organisations. On the one hand, this shortens the communication gap between domain experts and IT specialists. On the other hand, this permits to clarify the characteristics of software systems introduced to provide automatic support for such activities. Nevertheless, the lack of formal semantics hinders the automatic verification of relevant properties. This paper presents a novel verification framework for BPMN 2.0, called BProVe. It is based on an operational semantics, implemented using MAUDE, devised to make the verification general and effective. A complete tool chain, based on the Eclipse modelling environment, allows for rigorous modelling and analysis of Business Processes. The approach has been validated using more than one thousand models available on a publicly accessible repository. Besides showing the performance of BProVe, this validation demonstrates its practical benefits in identifying correctness issues in real models.

This demo introduces BProVe, a tool supporting automated verification of Business Process models. BProVe analysis is based on a formal operational semantics defined for the BPMN 2.0 modelling language, and is provided as a freely accessible service that uses open standard formats as input data. Furthermore a plug-in for the Eclipse platform has been developed making available a tool chain supporting users in modelling and visualising, in a friendly manner, the results of the verification. Finally we have conducted a validation through more than one thousand models, showing the effectiveness of our verification tool in practice. (Demo video: https://youtu.be/iF5OM7vKtDA).

A Wireless Sensor Network (WSN) is composed of distributed sensors with limited processing capabilities and energy restrictions. These unique attributes pose new challenges amongst which prolonging the WSN lifetime is one of the most important. Clustering is an energy efficient routing technique that has been widely applied to report data from the WSN nodes to a centralised Base Station. A plethora of different clustering protocols have been proposed. Some protocols are based on equal-sized clusters while others use clusters of unequal size. Some others make use of rotation techniques to reduce the amount of cluster head elections. When different clustering approaches are presented different simulation settings are used. In this paper we perform a comparison study of HEED based clustering protocols that are HEED, UHEED, RUHEED and a novel variation of R-HEED that is ER-HEED. We have considered the same network model, the same energy consumption model and we have compared the lifetime of the protocols by considering various case studies. Our comparison study shows that the selection of the protocol to be used depends on the case study and the WSN lifetime measure that is considered.

Multitenancy is one the new property of cloud computing paradigm that change the way of develop software. This concept consists in the aggregation of different tenant in one single istance in contrast with the classic single-tenant concept. The aim of multitenancy is the reduction of costs, the hardware needed is less than single-tenant application, and also the mantainance of the system is less expensive. On the other hand, applications need an high configuration level in order to satisfy the requirements of each tenant. In this paper is presented a pattern that enable legacy applications to handle a multitenancy database. After the presentation of the different approach that implements multitenancy at database system, it is proposed the pattern that aims to interact with this kind of database managing the different customization of different tenant at database level. Copyright © 2016 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved.

Applications and services hosted in the cloud are increasing continuously. Cloud technology offers important perspectives (performance, high availability, elasticity) and it enables new business models. Unfortunately, this new paradigm faces unprecedent requirements not addressed in legacy application (multi-tenancy, scalability, etc.). This leads to complex re-engineering phases in order to to migrate existing software into a cloud environment. Before starting a migration, it is important to analyze the cloud compliance of the application, what to expect after the migration and the effort required to fulfill these expectations. This paper assesses a way to extract an index that describes the feasibility of the re-engineering. We test the metric with a real application that needs to be migrated to a private cloud.

A Service Oriented Architecture aims to facilitate interaction of loosely coupled services in large-scale dynamic systems. Despite a decade’s active research and development, Web Services still remain undependable (Bourne et al., 2012). In literature many proposals attempt to overcome interoperability issues, particularly typical of not-orchestrated Web Service (WS) compositions. Although these techniques aid to discover potential interoperability mismatches, they do not fit well with flexibility and dynamism, desirable characteristics e.g. in choreographies. Here unsafe run-time changes may compromise a correct execution. To support such dynamism and to mitigate the effects of such failures, we propose a flexible architecture able to realize dynamic WS compositions, supporting run-time monitoring and verification techniques. The technique we chose is a novel run-time algorithm capable to predict potential failures that can happen in near future states of a choreography. It a dmits an integration ”a-priori” and monitors the run-time services behaviour to provide information about possible errors when these can happen.

In a service-oriented architecture, systems communicate by exchanging messages. In this work, we propose a formal model based on OCL-constrained UML Class diagrams and a methodology based on Alloy Analyzer respectively for describing and verifying any first-order constrained client-server conversations. This framework allows us to verify conversation protocol designs at a fairly detailed level and to check first-order logic constraints on both message flows and message contents.

BACKGROUND: Brain, heart and skeletal muscle share similar properties of excitable tissue, featuring both discrete behavior (all-or-nothing response to electrical activation) and continuous behavior (recovery to rest follows a temporal path, determined by multiple competing ion flows). Classical mathematical models of excitable cells involve complex systems of nonlinear differential equations. Such models not only impair formal analysis but also impose high computational demands on simulations, especially in large-scale 2-D and 3-D cell networks. In this paper, we show that by choosing Hybrid Automata as the modeling formalism, it is possible to construct a more abstract model of excitable cells that preserves the properties of interest while reducing the computational effort, thereby admitting the possibility of formal analysis and efficient simulation. RESULTS: We have developed CellExcite, a sophisticated simulation environment for excitable-cell networks. CellExcite allows the user to sketch a tissue of excitable cells, plan the stimuli to be applied during simulation, and customize the diffusion model. CellExcite adopts Hybrid Automata (HA) as the computational model in order to efficiently capture both discrete and continuous excitable-cell behavior. CONCLUSIONS: The CellExcite simulation framework for multicellular HA arrays exhibits significantly improved computational efficiency in large-scale simulations, thus opening the possibility for formal analysis based on HA theory. A demo of CellExcite is available at http://www.cs.sunysb.edu/~eha/.

2006 was a special year for both mathematical logic and computer science, as it celebrated Gödel's centenary. Although Gödel's work was mainly concerned with mathematics and metamathematics, the crucial role it had in the foundation of modern theoretical computer science is undeniable: for instance, one only has to remember Gödel's contributions to the birth of recursion theory as well as his part in the debate in the nineteen thirties on the subject of the Church Thesis.

The adoption of agent technologies and multi-agent systems constitutes an emerging area in bioinformatics. In this article, we report on the activity of the Working Group on Agents in Bioinformatics (BIOAGENTS) founded during the first AgentLink III Technical Forum meeting on the 2nd of July, 2004, in Rome. The meeting provided an opportunity for seeding collaborations between the agent and bioinformatics communities to develop a different (agent-based) approach of computational frameworks both for data analysis and management in bioinformatics and for systems modelling and simulation in computational and systems biology. The collaborations gave rise to applications and integrated tools that we summarize and discuss in context of the state of the art in this area. We investigate on future challenges and argue that the field should still be explored from many perspectives ranging from bio-conceptual languages for agent-based simulation, to the definition of bio-ontology-based declarative languages to be used by information agents, and to the adoption of agents for computational grids.

BACKGROUND: An in-silico experiment can be naturally specified as a workflow of activities implementing, in a standardized environment, the process of data and control analysis. A workflow has the advantage to be reproducible, traceable and compositional by reusing other workflows. In order to support the daily work of a bioscientist, several Workflow Management Systems (WMSs) have been proposed in bioinformatics. Generally, these systems centralize the workflow enactment and do not exploit standard process definition languages to describe, in order to be reusable, workflows. While almost all WMSs require heavy stand-alone applications to specify new workflows, only few of them provide a web-based process definition tool. RESULTS: We have developed BioWMS, a Workflow Management System that supports, through a web-based interface, the definition, the execution and the results management of an in-silico experiment. BioWMS has been implemented over an agent-based middleware. It dynamically generates, from a user workflow specification, a domain-specific, agent-based workflow engine. Our approach exploits the proactiveness and mobility of the agent-based technology to embed, inside agents behaviour, the application domain features. Agents are workflow executors and the resulting workflow engine is a multiagent system - a distributed, concurrent system--typically open, flexible, and adaptative. A demo is available at http://litbio.unicam.it:8080/biowms. CONCLUSION: BioWMS, supported by Hermes mobile computing middleware, guarantees the flexibility, scalability and fault tolerance required to a workflow enactment over distributed and heterogeneous environment. BioWMS is funded by the FIRB project LITBIO (Laboratory for Interdisciplinary Technologies in Bioinformatics).

We solve an open question of Milner [1984]. We define a set of so-called well-behaved finite automata that, modulo bisimulation equivalence, corresponds exactly to the set of regular expressions, and we show how to determine whether a given finite automaton is in this set. As an application, we consider the star height problem.

We tackle an open question of Milner (1984). We define a set of so-called well-behaved finite automata that, modulo bisimulation equivalence, corresponds exactly to the set of regular expressions.

In this paper we show how the expressive power of a language for the description of timed processes strongly affects the discriminating power of urgent and patient actions. In a sense, it studies the interplay between syntax and semantics of time-critical systems.

We provide a finite equational axiomatization for bisimulation equivalence of nondeterministic interpretation of regular expressions. Our axiomatization is heavily based on the one by Salomaa, that provided an implicative axiomatization for a large subset of regular expressions, namely all those that satisfy the non-empty word property (i.e. without 1 summands at the top level) in *-contexts. Our restriction is similar, it essentially amounts to recursively requiring that the non-empty word property be satisfied not just at top level but at any depth. We also discuss the impact on the axiomatization of different interpretations of the 0 term, interpreted either as a null process or as a deadlock.

The paper presents an approach to derive test plans for the conformance testing of a system implementation with respect to the formal description of its Software Architecture (SA). The SA describes a system in terms of its components and connections, therefore the derived test plans address the integration testing phase. We base our approach on a Labelled Transition System (LTS) modeling the SA dynamics, and on suitable abstractions of it, the Abstract Labelled Transition Systems (ALTSs). ALTSs oer specic views of the SA dynamics by concentrating on relevant features and abstracting away from uninteresting ones. ALTS is a tool we provide the software architect with allow him/her to focus on relevant behavioral patterns and more easily identify those ones that are more meaningful for validation purposes. Intuitively deriving an adequate set of functional test classes means deriving a set of paths appropriately covering the ALTS. In the paper we describe our approach in the scope of a...

In this paper we contrast (the core of) four well-known process algebras specifically enriched for the specification and verification of timed systems. The aim of this comparison is twofold. On one hand it permits to gain confidence on how time and time passing are modelled in the four different timed process algebras. On the other hand, it establishes conditions under which mappings from a calculus to another can be provided which preserve (strong bisimulation-based) behavioural equivalence.

Three of the rewriting systems used by Degano, De Nicola and Montanari to provide Milner's CCS with a causality based semantics are compared by using also a fourth intermediate one. These rewriting systems have been used to associate Petri nets, Labelled Event Structures and structured sets of partial orderings to CCS terms. It is proved that the four rewriting systems yield computations from which the same causality relations among the executed actions can be extracted, thus it is established that the four partial ordering transitional semantics do coincide.