Recently, a distributed middleware application called contract automata runtime environment (CARE) has been introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling, verification and testing of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilising exhaustive and statistical model checking techniques. Abstract tests are generated from the Uppaal models that are concretised for testing CARE. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and generating concrete tests from the abstract model, addressing the issues that have been identified and fixed.

Process mining techniques enable organizations to gain insights into their business processes through the analysis of execution records (event logs) stored by information systems. While most process mining efforts focus on intra-organizational scenarios, many real-world business processes span multiple independent organizations. Inter-organizational process mining, though, faces significant challenges, particularly regarding confidentiality guarantees: The analysis of data can reveal information that the participating organizations may not consent to disclose to one another, or to a third party hosting process mining services. To overcome this issue, this paper presents CONFINE, an approach for secrecy-preserving inter-organizational process mining. CONFINE leverages Trusted Execution Environments (TEEs) to deploy trusted applications that are capable of securely mining multi-party event logs while preserving data secrecy. We propose an architecture supporting a four-stage protocol to secure data exchange and processing, allowing for protected transfer and aggregation of unaltered process data across organizational boundaries. To avoid out-of-memory errors due to the limited capacity of TEEs, our protocol employs a segmentation-based strategy, whereby event logs are transmitted to TEEs in smaller batches. We conduct a formal verification of our approach’s correctness alongside a security analysis on the guarantees provided by the TEE core. We test our implementation using real-world and synthetic data to assess memory usage. Our experiments show that an incremental approach to segment processing in discovery and conformance checking is preferable over non-incremental strategies as the former maintains memory usage trends within a narrow range at runtime, whereas the latter exhibit high peaks towards the end of the execution. Furthermore, our results confirm that our prototype can handle real-world workloads without out-of-memory failures. The scalability tests reveal that memory usage grows logarithmically as the event log size increases. Memory consumption grows linearly with the number of provisioning organizations, indicating potential scalability limitations and opportunities for further optimizations.

Team automata were introduced as a flexible extension of I/O automata to model collaborative behaviour in component-based and distributed systems. Their distinctive features include multi-party communication and a liberal synchronisation mechanism: components may jointly execute shared actions according to synchronisation policies that specify which subsets of components participate as senders or receivers. While this makes team automata well suited for modelling coordination, existing communication is synchronous and therefore insufficient for capturing certain behavioural aspects (e.g., due to message reordering) of modern networks and distributed systems, in which communication is typically asynchronous and message delays are unpredictable. In this paper, we introduce asynchronous team automata (ATeams), which extend team automata with buffers to model asynchronous communication, in addition to conventional synchronous interaction. ATeams support individual interactions involving multiple senders and receivers, unlike well-known asynchronous models such as communicating finite-state machines and multi-party session types. We formalise the syntax and operational semantics of ATeams, study well-formedness and well-behavedness conditions, and present the prototypical A-Team tool that supports specification, animation and automated checks. This proposes ATeams as a unifying semantic foundation for modelling and analysis of heterogeneous synchronous–asynchronous multi-party interactions.

We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.

The online monitoring of collaborative business processes involves the integration of event data sourced from various information systems into a unified process state. The transmission of process records across organizational boundaries poses significant data secrecy and security challenges. In this context, organizations may be reluctant to outsource sensitive data with their collaborators to update a global process state. In this paper, we propose ProMTEE, a novel framework designed to tackle these challenges by resorting to trusted applications running in Trusted Execution Environments (TEEs). To showcase the potential of ProMTEE, we contextualize its four-staged interaction protocol within the realm of two online monitoring tasks, namely, control flow tracking and compliance monitoring. We verify the security of our solution through a threat analysis against a set of security requirements derived from a supply-chain scenario. In addition, we conduct an experimental assessment of our proof-of-concept implementation with tests on memory usage and latency using real-world datasets.

The project ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims to provide novel solutions for the evaluation of RAMS requirements as well as to present trade-offs between dependability attributes and energy consumption in complex railway systems, leveraging both qualitative and quantitative evaluation methods. To this end, case studies concerning distributed interlocking systems, standard interfaces, and railroad switch heaters are considered, comprising different challenging scenarios, notably representative of the complexity of railway systems. In this paper, we illustrate the objectives of the project and the activities planned to address them, devising future steps to integrate the envisaged contributions within a unified framework.

Contract automata allow to formally define the behaviour of service contracts in terms of service offers and requests, some of which are moreover optional and some of which are necessary. A composition of contracts is said to be in agreement if all service requests are matched by corresponding offers. Whenever a composition of contracts is not in agreement, it can be refined to reach an agreement using the orchestration synthesis algorithm. This algorithm is a variant of the synthesis algorithm used in supervisory control theory and it is based on the fact that optional transitions are controllable, whereas necessary transitions are at most semi-controllable and cannot always be controlled. In this paper, we present advancements of the orchestration synthesis for contract automata. Notably, we identify the existing limits of the orchestration synthesis and propose a novel orchestration synthesis along with additional constructs to enhance the expressiveness and scalability of contract automata. The proposed advancements have been implemented and experimented on two case studies, one of which originates from the railway domain and the other is a card game.

Inter-organizational business processes involve multiple independent organizations collaborating to achieve mutual interests. Process mining techniques have the potential to allow these organizations to enhance operational efficiency, improve performance, and deepen the understanding of their business based on the recorded process event data. However, inter-organizational process mining faces substantial challenges, including topical secrecy concerns: The involved organizations may not be willing to expose their own data to run mining algorithms jointly with their counterparts or third parties. In this paper, we introduce CONFINE, a novel approach that unlocks process mining on multiple actors' process event data while safeguarding the secrecy and integrity of the original records in an inter-organizational business setting. To ensure that the phases of the presented interaction protocol are secure and that the processed information is hidden from involved and external actors alike, our approach resorts to a decentralized architecture comprised of trusted applications running in Trusted Execution Environments (TEEs). We show the feasibility of our solution by showcasing its application to a healthcare scenario and evaluating our implementation in terms of memory usage and scalability on real-world event logs.

Mutation Testing (MT) is a technique employed to assess the efficacy of tests by introducing artificial faults, known as mutations, into the system. The goal is to evaluate how well the tests can detect these mutations. These artificial faults are generated using mutation operators, which produce a set of mutations derived from the original system. Mutation operators and frameworks exist for a variety of programming languages, and model-based mutation testing is gaining traction, particularly for timed safety-critical systems. This paper focuses on extending MT to Networks of Timed Automata (NTAs), an area that has not been extensively explored. We introduce mutation operators designed for NTAs specified in UPPAAL, aiming to create temporal interaction faults. We assess the effectiveness of these operators on five UPPAAL NTAs sourced from the literature, specifically examining the generation of equivalent and duplicate mutants. Our results demonstrate a varied prevalence of equivalent mutants (from 12% to 71%) while the number of duplicates is less. In all cases, timed bisimulation was able to process each mutant pair in less than one second.

In the contemporary business landscape, collaboration across multiple organizations offers a multitude of opportunities, including reduced operational costs, enhanced performance, and accelerated technological advancement. The application of process mining techniques in an inter-organizational setting, exploiting the recorded process event data, enables the coordination of joint effort and allows for a deeper understanding of the business. Nevertheless, considerable concerns pertaining to data confidentiality emerge, as organizations frequently demonstrate a reluctance to expose sensitive data demanded for process mining, due to concerns related to privacy and security risks. The presence of conflicting interests among the parties involved can impede the practice of open data sharing. To address these challenges, we propose our approach and toolset named CONFINE, which we developed with the intent of enabling process mining on process event data from multiple providers while preserving the confidentiality and integrity of the original records. To ensure that the presented interaction protocol steps are secure and that the processed information is hidden from both involved and external actors, our approach is based on a decentralized architecture and consists of trusted applications running in Trusted Execution Environments (TEE). In this demo paper, we provide an overview of the core components and functionalities as well as the specific details of its application.

Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Coherent MTS (CMTS) have been introduced to model Software Product Lines (SPL) based on a correspondence between the necessary and permitted modalities of MTS transitions and their associated actions, and the core and optional features of SPL. In this paper, we address open problems of the coherent fragment of MTS and introduce the notions of refinement and thorough refinement of CMTS. Most notably, we prove that refinement and thorough refinement coincide for CMTS, while it is known that this is not the case for MTS. We also define (thorough) equivalence and strong bisimilarity of both MTS and CMTS. We show their relations and, in particular, we prove that also strong bisimilarity and equivalence coincide for CMTS, whereas they do not for MTS. Finally, we extend our investigation to CMTS equipped with Constraints (MTSC), originally introduced to express alternative behaviour, and we prove that novel notions of refinement and strong thorough refinement coincide for MTSC, and so do their extensions to strong (thorough) equivalence and strong bisimilarity.

The contract automata runtime environment (CARE) is a distributed middleware application recently introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling and verification of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilizing exhaustive and statistical model checking techniques. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and address the issues that have been identified and fixed.

Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Modal refinement (≼_m) of MTS represents a step of the design process, namely the one in which some optional behaviour is discarded while other optional behaviour becomes necessary. Whenever two MTS are not in modal refinement relation, it could still be the case that the set of implementations of one MTS is included in the set of implementations of the other. The challenge of devising an alternative notion of modal refinement that is both sound and complete with respect to the set of implementations, without disregarding valuable implementations, remains open. We introduce a subset of MTS called Non-reducible Modal Transition Systems (NMTS), together with a novel refinement relation ≼_n for NMTS. We illustrate through examples the additional constraints imposed by NMTS. Furthermore, we discuss a property holding for NMTS whose implementations are non-deterministic.

The integration of circular economy (CE) models into everyday contexts generates huge amount of data involved in goods tracking and tokenization procedures.The sector of blockchain platforms is extremely varied, and the choice of the proper technology is not easy.It is important that the selection is conducted consistently with respect to the CE models.With this study, we present a performance index named Blockchain Circular Economy Index (BCEI).BCEI, obtained through Multicriteria Decision Analysis and Analytic Hierarchy Process, aims to measure the suitability of blockchain platforms to the needs highlighted by a CE scenario.The present study is contextualized by comparing six blockchain platforms, for each of which, the related BCEI is calculated.The results of the analysis show that transaction fee and energy consumption are the two most critical parameters.In addition, the results show the lack of a leading blockchain technology in CE models.Thus, there is a market space that can be exploited given the growing interest in digital and sustainable issues.

Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of applications from contract automata specifications. We present CARE, a new runtime environment to coordinate services implementing contracts that guarantees the adherence of the implementation to its contract. We discuss how CARE can be adopted to realise contract-based applications, its formal guarantees, and we identify the responsibilities of the involved business actors. Experiments show the benefits of adopting CARE with respect to manual implementations.

The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to real-time systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.

We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools CATLib and VoxLogicA to interact in a fully automated way. The Contract Automata Library (CATLib) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (VoxLogicA) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with CATLib, while the properties to enforce are defined by means of spatial model checking of the images with VoxLogicA. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain’s performance also considering several recent improvements.

Decentralization initiatives such as Solid, Digi.me, and ActivityPub aim to give data owners more control over their data and to level the playing field by enabling small companies and individuals to gain access to data, thus stimulating innovation. However, these initiatives typically use access control mechanisms that cannot verify compliance with usage conditions after access has been granted to others. In this paper, we extend the state of the art by proposing a resource governance conceptual framework, entitled ReGov, that facilitates usage control in decentralized web environments. We subsequently demonstrate how our framework can be instantiated by combining blockchain and trusted execution environments. Through blockchain technologies, we record policies expressing the usage conditions associated with resources and monitor their compliance. Our instantiation employs trusted execution environments to enforce said policies, inside data consumers' devices. We evaluate the framework instantiation through a detailed analysis of requirments derived from a data market motivating scenario, as well as an assessment of the security, privacy, and affordability aspects of our proposal.