Managing consent for Electronic health record (EHR) faces critical challenges in modern healthcare systems. Paper-based consent mechanisms lack granular permission control and cannot scale to manage millions of patients. While blockchain technology offers immutable audit trails essential for sensitive medical data, its low transaction throughput makes cross-patient aggregation queries infeasible. We present a novel protocol that maintains blockchain's cryptographic guarantees while delegating queries to high-performance lookup tables, enabling fast category lookups across millions of patients. Our system combines hierarchical consent trees, blockchain audit trails, and event-driven synchronization with reconciliation mechanisms. Additionally, we implement automated GDPR compliance verification through zero-knowledge proofs, enabling processors to cryptographically prove compliance without exposing processed data. Evaluation demonstrates practical query performance enabling real-time dataset compilation while maintaining cryptographic integrity and sub-second proof verification.

Maintaining consistency between business process models and their textual descriptions is critical for operational clarity, compliance, and communication. However, as process models evolve, updating documentation remains costly and error-prone. Existing methods often require manual rewriting or full text regeneration, discarding valuable domain-specific language. This paper presents an edit-based synchronization approach that incrementally updates textual descriptions to reflect changes in Business Process Model and Notation(BPMN) diagrams while preserving unaffected content. We propose two complementary algorithms: the Longest Common Execution Subsequence (LCES) approach for balanced acyclic models, and a heuristic beam search for more complex structures with loops and unbalanced gateways. The resulting transformation steps are translated into structured prompts guiding a large language model to produce minimal, style-consistent revisions. A prototype system demonstrates high semantic accuracy and stylistic coherence across diverse process evolution scenarios.

Background Topology and Orchestration Specification for Cloud Applications (TOSCA) is a specification language used for modelling topology and orchestration of cloud applications. This language particularly allows the description of workflows that can be used for specifying management tasks such as (un)deployment plans.Motivations This textual language for describing TOSCA workflows does not provide any visual notation for graphically designing or observing the corresponding workflows. Moreover, this specification language is error-prone and can be source of mistakes during the writing of the management plans.Methods In this article, we propose a transformation from TOSCA to the graphical Business Process Model and Notation (BPMN), which allows the visualisation of TOSCA workflows. We also provide automated verification techniques for analysing TOSCA (un)deployment workflows in terms of functional and architectural properties as well as execution times. The transformation and verification steps are achieved in a fully automated way.Results This approach computes BPMN models and verification results within a reasonable time on realistic applications.

Context: A business process describes a set of structured tasks that follow a specific order and results in a product or service. Comparing two different versions of a same process is crucial for tackling several problems such as process analysis, evolution or refactoring. Objective: The goal of this paper is to propose new techniques for automatically comparing two BPMN processes from a semantic point of view in an efficient way in terms of computational complexity. Methods: In order to compute this comparison efficiently, our approach detects the syntactic differences between the two processes, and then compares the semantic models of both processes only for these differences-Labeled Transition Systems are used to represent the semantics of BPMN processes. This procedure thus avoids the comparison of the entire semantic models, which may be very costly. The notion of comparison used in this work rely on the congruence of the operators underlying the syntactic matching and on behavioral equivalences and bisimulations. Results: In this paper, we present efficient techniques for automating the semantic comparison of BPMN processes. Our approach is fully automated using a toolchain that we implemented. Conclusion: Experimental results were carried out to evaluate the performance of our solution. These results show that the comparison computation is much faster with our approach and toolchain than with other alternative techniques.

A business process is defined as a set of tasks executed in a certain order to achieve a specific goal. Business Process Model and Notation (BPMN) has become the standard modelling language for describing and developing business processes. One of the main challenges in the business process management area is to provide techniques and tools for analysing and optimising processes, which are necessary for example to avoid bugs or unexpected process executions. However, modelling and debugging processes is a difficult task. This paper presents GIVUP, a tool that takes as input descriptions of a process and of a functional property written in natural language. GIVUP transforms the textual process into BPMN and the textual property into the corresponding Linear Temporal Logic (LTL) formula. It then verifies whether the BPMN process satisfies the property or not, in which case it returns a diagnostic. These steps are achieved by using several internal transformations and model checking techniques. This approach is helpful for any kind of users, either novices or experts, and can be used during several stages of the lifecycle of a process, such as the design phase or any refinement phase. GIVUP is freely accessible online, and a demo video can be found at: https://youtu.be/MdM4NaPQXMk.

EHRs or Electronic Health Records are digital medical records regarding the health of patients. They are sensitive in nature and their storage and management needs to adhere to strict guidelines. Multiple applications depend on this data for efficiently managing their healthcare requirements. This work proposes FaSTr, a solution based on blockchain that enables Fast, Secure and Transparent communication and collaboration between applications, by providing services. These services are accessible via defined protocols, such as APIs. FaSTr exposes secure API endpoints to provide functionality to manage and share EHRs. This is achieved with the help of several novel ideas: A compatibility layer that improves interoperability, an API server that exposes important endpoints for services and a private network of nodes for each service resulting in high availability and robustness. Finally, performance evaluations demonstrate the real-world usability and scalability of FaSTr.

The digitisation of personal health information (PHI) through electronic health record (EHR) is now widely adopted due to their efficiency in terms of cost, storage, processing, and the subsequent quality of delivering patient care. However, security concerns remain one of its major setback. In order to handle EHR, institutions need to comply with their local government security regulations. These regulations control to which extent health data can be processed, transmitted, and stored as well as define how misuses are addressed. φ -comp has been proposed as an industrial solution for monitoring, assessing, and evaluating the compliance of health applications with respect to defined security regulations. φ -comp is able to assess the level of security risk of an application at runtime and to automatically perform the required mitigation actions to recover a compliant environment. Since the risk associated to sensitive health data is critical, there is a need of guarantees in terms of correctness of the φ -comp approach. In this paper, we first present a formal specification of φ -comp representing all the components of the solution as well as their behaviour, that is, the way they all interact together to implement the whole approach from monitoring to mitigation. In a second step, some important properties of interest are formalised and analysed using model checking techniques on several realistic applications.

A business process is a collection of structured tasks corresponding to a service or a product. Business processes do not execute once and for all, but are executed multiple times resulting in multiple instances. In this context, it is particularly difficult to ensure correctness and efficiency of the multiple executions of a process. In this paper, we propose to rely on Probabilistic Model Checking (PMC) to automatically verify that multiple executions of a process respect some specific probabilistic property. This approach applies at runtime, thus the evaluation of the property is periodically verified and the corresponding results updated. However, we go beyond runtime PMC for BPMN, since we propose runtime enforcement techniques to keep executing the process while avoiding the violation of the property. To do so, our approach combines monitoring techniques, computation of probabilistic models, PMC, and runtime enforcement techniques. The approach has been implemented as a toolchain and has been validated on several realistic BPMN processes.

Resource allocation is a critical problem in business processes due to the simultaneous execution of tasks and resource sharing among them. The number of allocated resources affects both the execution cost and time of the process. In the context of runtime processes, a well-defined resource allocation strategy is essential for optimising waiting times and costs by mitigating delays and enhancing resource utilisation. This paper introduces a novel approach to dynamically adjust resource allocation during the execution of BPMN (Business Process Model and Notation) processes. The BPMN process is monitored in real-time, and the execution traces produced during its multiple executions are analysed. These execution traces are used to compute various properties or metrics of interest, including resource usage and average execution time. The approach then relies on predictive analytics to compute the future values of the aforementioned metrics. Based on these predicted results, strategies for the dynamic allocation of resources are defined, which anticipate changes in resource usage and thus dynamically update the number of resources in advance. This approach is fully automated using a toolchain and has been validated with multiple examples.

Model checking automatically verifies that a model, e.g., a Labelled Transition System (LTS), obtained from higher-level specification languages, satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, but this counterexample does not precisely identify the source of the bug. Moreover, manually correcting the given specification or model can be a painful and complicated task. In this paper, we propose some techniques for computing patches that can correct an erroneous specification violating an eventually property. These techniques first extract from the whole behavioural model the part which does not satisfy the given property. In a second step, this erroneous part is analysed using several algorithms in order to compute the minimal number of patches in the specification so as to make it satisfy the given property. The approach is fully automated using a tool we implemented and applied on a series of examples for validation purposes.

Modelling and designing business processes has become a crucial activity for companies in the last 20 years. As a consequence, multiple workflow modelling notations were proposed. Business Process Modelling Notation (BPMN) is one of them and is now considered as the de facto standard for process modelling. The BPMN notation offers a rich syntax that requires a certain level of expertise before being able to write correct and well-structured processes corresponding to some expected requirements. The BPMN modelling phase can thus be tedious and error-prone if carried out by non-experts. The main goal of the approach presented in this paper is to help users modelling BPMN processes. To do so, the approach takes as input the requirements of the user in a textual format informally describing the tasks and their ordering constraints, and generates as output a BPMN process satisfying them. The solution has been implemented as a tool that was applied on a large number of examples for evaluation purposes.

This work envisions industrial control systems that can reliably adapt to requirements. We rely on the international standard IEC 61499 to achieve this goal. The standard allows downtimeless system evolution such that an application can be modified at runtime to satisfy the requirements. However, an IEC 61499 application consisting of multiple Function Blocks (FBs) can be modified in many different ways, such as inserting or deleting FBs, creating new FBs with their respective internal behaviours, and adjusting the connections between FBs. These changes require considerable effort and cost, and there is no guarantee to satisfy the requirements. This paper applies runtime enforcement techniques for supporting adaptive IEC 61499 applications. This set of techniques can modify the runtime behaviour of a system according to specific requirements. Our approach begins with specifying the requirements as a state machine-based notation called contract automaton. This automaton is then used to synthesise an enforcer as an FB. Finally, the new FB is integrated into the application to execute according to the requirements. A tool support is developed to automate the approach. Experiments were performed to evaluate the performance of enforcers by measuring the execution time of several applications before and after the integration of enforcers.

IEC 61499 is a standard for developing industrial automation systems. It is known for its reusability, reconfigurability, interoperability, and portability. However, during their life cycle, industrial systems need to evolve according to requirements, and modifying the applications to satisfy these requirements can be complex and error-prone. This paper proposes techniques to guide the evolution of IEC 61499 applications. Given an initial application and the evolution requirements, we generate guidelines for modifying the application to satisfy the requirements. The application is first translated into a behavioural model describing all possible sequences of events the application can trigger. We then apply algorithms to extract relevant submodels of the application and modify them according to the requirements. Finally, the submodels are analysed to generate guidelines for modifying the application. These guidelines can bridge the gap between the requirements and the target application. Instead of only considering the requirements when exploring possible modifications, the developers can use the guidelines to make necessary changes to the application. A mixing tank system is used as a running example to illustrate the approach. In addition, a prototype to automate the evolution techniques is developed.

The ever-increasing complexity of industrial control systems generates a demand for reliable development methods. IEC 61499, a recent industrial standard, helps to develop complex distributed systems based on their positive characteristics, namely reusability, reconfigurability, interoperability, and portability. Formal verification techniques, such as model checking, have been proposed to ensure the correctness of these systems during the design time. However, they do not consider the presence of the environment that can impact the application behaviour at runtime. This work combines design time and runtime analyses to apply probabilistic model checking on an IEC-61499-based manufacturing application. We present several probabilistic properties to be checked. The results are visualised graphically to be analysed, which allows one to optimise the system's quantitative features, such as productivity.

Business process optimisation is a strategic activity in organisations because of its potential to increase profit margins and reduce operational costs. In this paper, we focus on a specific technique used for process optimisation known as process refactoring. In this work, a process is described using BPMN extended with quantitative aspects for modelling execution times and resources associated with tasks. A process is not executed once but multiple times, and multiple concurrent executions of a process compete for using the shared resources. In this context, we propose a refactoring approach whose goal is to reduce the total execution time of the process and optimise the usage of the shared resources. To do so, we first analyse the given process in terms of task dependency and resource usage, and then rely on these results to restructure the process and return an optimal version of it. This process refactoring technique is fully automated by a tool that we implemented and applied on several examples for validation purposes.

A business process is a collection of related tasks organized in a specific order whose overall execution solves a specific service or product. BPMN has become the standard workflow-based notation for developing business processes. Designing business processes using BPMN is however error-prone. Recent works have proposed verification techniques for analyzing processes and for detecting possible issues. In particular, model checking is an established technique for automatically verifying that a model (e.g., a BPMN process) satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the process is not an easy task, especially if the counterexample is not expressed using the original notation (BPMN here). In this paper, we focus on the model checking of BPMN processes. When properties are violated, we propose to transform counterexamples back on to the original BPMN process in order to simplify the debugging steps. To do so, we rely on coloration techniques. The approach proposed in this paper is fully automated using several tools and was validated on many examples.

Business Process Model and Notation (BPMN) is a standard business process modelling language that allows users to describe a set of structured tasks, which results in a service or product. Before running a BPMN process, the user often has no clear idea of the probability of executing some task or specific combination of tasks. This is, however, of prime importance for adjusting resources associated with tasks and thus optimising costs. In this paper, we define an approach to perform probabilistic model checking of BPMN models at runtime. To do so, we first transform the BPMN model into a Labelled Transition System (LTS). Then, by analysing the execution traces obtained when running multiple instances of the process, we can compute the probability of executing each transition in the LTS model, and thus generate a Probabilistic Transition System (PTS). Finally, we perform probabilistic model checking for verifying that the PTS model satisfies a given probabilistic property. This verification loop is applied periodically to update the results according to the execution of the process instances. All these steps are implemented in a tool chain, which was applied successfully to several realistic BPMN processes.

Industrial automation is a complex process involving various stakeholders. The international standard IEC 61499 helps to specify distributed automation using a generic architectural model, targeting the technical development of the automation. However, analysing the correctness of IEC 61499 models remains a challenge because of their informal semantics and distributed logic. We propose new verification techniques for IEC 61499 applications. These techniques rely on the concept of runtime enforcement, which can be applied to systems for preventing bad behaviours from happening. The main idea of our approach is to integrate an enforcer in the application for allowing it to respect specific properties when executing. The techniques begin with the definition of a property. The language of this property supports features such as discarding and replacing events. Next, this property is used to synthesise an enforcer in the form of a function block. Finally, the synthesised enforcer is integrated into the application. Our approach is illustrated on a realistic example and fully automated.

Business process optimisation is a strategic activity in organisations because of its potential to increase profit margins and reduce operational costs. One of the main challenges in this context is concerned with the problem of optimising the allocation and sharing of resources. In this work, processes are described using the BPMN notation extended with an explicit description of execution time and resources associated with tasks, and can be concurrently executed multiple times. First, a simulation-based approach for computing certain metrics of interest, such as average execution time or resource usage, is presented. This approach applies off-line and is static in the sense that the number of resources does not evolve over the time of the simulation. In a second step, an alternative approach is presented, which works online, thus requiring the instrumentation of an existing platform for retrieving information of interest during the processes’ execution. This second approach is dynamic because the number of resource replicas is updated over the time of the execution. This paper aims at stressing pros and cons of both approaches, and at showing how they complement each other.