-
Meshing of High-Dimensional Toroidal Manifolds from Quasi-Periodic Three-Body Problem Dynamics using Parameterization via Discrete One-Forms
Authors:
Dante Basile,
Xavier Tricoche,
Martin Lo
Abstract:
High-dimensional visual computer models are poised to revolutionize the space mission design process. The circular restricted three-body problem (CR3BP) gives rise to high-dimensional toroidal manifolds that are of immense interest to mission designers. We present a meshing technique which leverages an embedding-agnostic parameterization to enable topologically accurate modelling and intuitive vis…
▽ More
High-dimensional visual computer models are poised to revolutionize the space mission design process. The circular restricted three-body problem (CR3BP) gives rise to high-dimensional toroidal manifolds that are of immense interest to mission designers. We present a meshing technique which leverages an embedding-agnostic parameterization to enable topologically accurate modelling and intuitive visualization of toroidal manifolds in arbitrarily high-dimensional embedding spaces. This work describes the extension of a discrete one-form-based toroidal point cloud meshing method to high-dimensional point clouds sampled along quasi-periodic orbital trajectories in the CR3BP. The resulting meshes are enhanced through the application of an embedding-agnostic triangle-sidedness assignment algorithm. This significantly increases the intuitiveness of interpreting the meshes after they are downprojected to 3D for visualization. These models provide novel surface-based representations of high-dimensional topologies which have so far only been shown as points or curves. This success demonstrates the effectiveness of differential geometric methods for characterizing manifolds with complex, high-dimensional embedding spaces, laying the foundation for new models and visualizations of high-dimensional solution spaces for dynamical systems. Such representations promise to enhance the utility of the three-body problem for the visual inspection and design of space mission trajectories by enabling the application of proven computational surface visualization and analysis methods to underlying solution manifolds.
△ Less
Submitted 3 April, 2025;
originally announced April 2025.
-
Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
Authors:
Davide Basile
Abstract:
Recently, a distributed middleware application called contract automata runtime environment ({\tt 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 {\tt CARE}. We provide a formalisation as a network of stochastic timed automata. The model is verified against the…
▽ More
Recently, a distributed middleware application called contract automata runtime environment ({\tt 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 {\tt CARE}. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool {\sc Uppaal}, utilising exhaustive and statistical model checking techniques. Abstract tests are generated from the {\sc Uppaal} models that are concretised for testing {\tt 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.
△ Less
Submitted 22 January, 2025;
originally announced January 2025.
-
CONFINE: Preserving Data Secrecy in Decentralized Process Mining
Authors:
Valerio Goretti,
Davide Basile,
Luca Barbaro,
Claudio Di Ciccio
Abstract:
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…
▽ More
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.
△ Less
Submitted 6 October, 2024;
originally announced October 2024.
-
AI-Assisted Diagnosis for Covid-19 CXR Screening: From Data Collection to Clinical Validation
Authors:
Carlo Alberto Barbano,
Riccardo Renzulli,
Marco Grosso,
Domenico Basile,
Marco Busso,
Marco Grangetto
Abstract:
In this paper, we present the major results from the Covid Radiographic imaging System based on AI (Co.R.S.A.) project, which took place in Italy. This project aims to develop a state-of-the-art AI-based system for diagnosing Covid-19 pneumonia from Chest X-ray (CXR) images. The contributions of this work are manyfold: the release of the public CORDA dataset, a deep learning pipeline for Covid-19…
▽ More
In this paper, we present the major results from the Covid Radiographic imaging System based on AI (Co.R.S.A.) project, which took place in Italy. This project aims to develop a state-of-the-art AI-based system for diagnosing Covid-19 pneumonia from Chest X-ray (CXR) images. The contributions of this work are manyfold: the release of the public CORDA dataset, a deep learning pipeline for Covid-19 detection, and the clinical validation of the developed solution by expert radiologists. The proposed detection model is based on a two-step approach that, paired with state-of-the-art debiasing, provides reliable results. Most importantly, our investigation includes the actual usage of the diagnosis aid tool by radiologists, allowing us to assess the real benefits in terms of accuracy and time efficiency. Project homepage: https://corsa.di.unito.it/
△ Less
Submitted 19 May, 2024;
originally announced May 2024.
-
Trusted Execution Environment for Decentralized Process Mining
Authors:
Valerio Goretti,
Davide Basile,
Luca Barbaro,
Claudio Di Ciccio
Abstract:
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 subs…
▽ More
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.
△ Less
Submitted 9 April, 2024; v1 submitted 19 December, 2023;
originally announced December 2023.
-
Non-reducible Modal Transition Systems
Authors:
Davide Basile
Abstract:
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 ($\preceq_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 re…
▽ More
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 ($\preceq_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 $\preceq_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.
△ Less
Submitted 7 March, 2024; v1 submitted 12 October, 2023;
originally announced October 2023.
-
A Blockchain-driven Architecture for Usage Control in Solid
Authors:
Davide Basile,
Claudio Di Ciccio,
Valerio Goretti,
Sabrina Kirrane
Abstract:
Decentralization initiatives like Solid enable data owners to control who has access to their data and to stimulate innovation by creating both application and data markets. Once data owners share their data with others, though, it is no longer possible for them to control how their data are used. To address this issue, we propose a usage control architecture to monitor compliance with usage contr…
▽ More
Decentralization initiatives like Solid enable data owners to control who has access to their data and to stimulate innovation by creating both application and data markets. Once data owners share their data with others, though, it is no longer possible for them to control how their data are used. To address this issue, we propose a usage control architecture to monitor compliance with usage control policies. To this end, our solution relies on blockchain and trusted execution environments. We demonstrate the potential of the architecture by describing the various workflows needed to realize a motivating use case scenario for data markets. Additionally, we discuss the merits of the approach from privacy, security, integrateability, and affordability perspectives.
△ Less
Submitted 9 October, 2023;
originally announced October 2023.
-
Research Challenges in Orchestration Synthesis
Authors:
Davide Basile,
Maurice H. ter Beek
Abstract:
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…
▽ More
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 fact, the resulting orchestration is such that as much of the behaviour in agreement is maintained. In this paper, we discuss recent developments of the orchestration synthesis algorithm for contract automata. Notably, we present a refined notion of semi-controllability and compare it with the original notion by means of examples. We then discuss the current limits of the orchestration synthesis algorithm and identify a number of research challenges together with a research roadmap.
△ Less
Submitted 23 August, 2023; v1 submitted 21 August, 2023;
originally announced August 2023.
-
Blockchain based Resource Governance for Decentralized Web Environments
Authors:
Davide Basile,
Claudio Di Ciccio,
Valerio Goretti,
Sabrina Kirrane
Abstract:
Decentralization initiatives such as Solid 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 employ access control mechanisms that cannot verify compliance with usage conditions after access has been granted to other…
▽ More
Decentralization initiatives such as Solid 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 employ 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 requirements derived from a data market motivating scenario, as well as an assessment of the security, privacy, and affordability aspects of our proposal.
△ Less
Submitted 24 April, 2023; v1 submitted 17 January, 2023;
originally announced January 2023.
-
A Runtime Environment for Contract Automata
Authors:
Davide Basile,
Maurice H. ter Beek
Abstract:
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…
▽ More
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.
△ Less
Submitted 15 March, 2023; v1 submitted 26 March, 2022;
originally announced March 2022.
-
Systematic Evaluation and Usability Analysis of Formal Tools for Railway System Design
Authors:
Alessio Ferrari,
Franco Mazzanti,
Davide Basile,
Maurice H. ter Beek
Abstract:
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require differen…
▽ More
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required.
To address this goal, this paper considers a set of 13 formal tools that have been used for railway system design, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools.
△ Less
Submitted 13 May, 2021; v1 submitted 27 January, 2021;
originally announced January 2021.
-
Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services
Authors:
Davide Basile,
Maurice H. ter Beek,
Rosario Pugliese
Abstract:
We present a number of contributions to bridging the gap between supervisory control theory and coordination of services in order to explore the frontiers between coordination and control systems. Firstly, we modify the classical synthesis algorithm from supervisory control theory for obtaining the so-called most permissive controller in order to synthesise orchestrations and choreographies of ser…
▽ More
We present a number of contributions to bridging the gap between supervisory control theory and coordination of services in order to explore the frontiers between coordination and control systems. Firstly, we modify the classical synthesis algorithm from supervisory control theory for obtaining the so-called most permissive controller in order to synthesise orchestrations and choreographies of service contracts formalised as contract automata. The key ingredient to make this possible is a novel notion of controllability. Then, we present an abstract parametric synthesis algorithm and show that it generalises the classical synthesis as well as the orchestration and choreography syntheses. Finally, through the novel abstract synthesis, we show that the concrete syntheses are in a refinement order. A running example from the service domain illustrates our contributions.
△ Less
Submitted 2 June, 2020; v1 submitted 2 October, 2019;
originally announced October 2019.
-
Automata for Specifying and Orchestrating Service Contracts
Authors:
Davide Basile,
Pierpaolo Degano,
Gian-Luigi Ferrari
Abstract:
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at sta…
▽ More
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the principals responsible for possible violations. To do that in the asynchronous case we resort to Linear Programming techniques. We also relate our automata with two logically based methods for specifying contracts.
△ Less
Submitted 27 December, 2016; v1 submitted 28 July, 2016;
originally announced July 2016.
-
From Orchestration to Choreography through Contract Automata
Authors:
Davide Basile,
Pierpaolo Degano,
Gian-Luigi Ferrari,
Emilio Tuosto
Abstract:
We study the relations between a contract automata and an interaction model. In the former model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The interaction model relies on channel-based asynchronous communication and choreography to coordinate distributed services.
We define a notion of strong a…
▽ More
We study the relations between a contract automata and an interaction model. In the former model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The interaction model relies on channel-based asynchronous communication and choreography to coordinate distributed services.
We define a notion of strong agreement on the contract model, exhibit a natural mapping from the contract model to the interaction model, and give conditions to ensure that strong agreement corresponds to well-formed choreography.
△ Less
Submitted 27 October, 2014;
originally announced October 2014.
