Modeling enterprise workflows has a direct impact on business process management, ensuring the eficient use of resources. Business processes span multiple organizational or system roles that perform tasks to achieve company goals. In this paper, we continue to extend an approach to role-based workflow modeling, based on a refinement that enables stepwise development of workflows from abstract models to detailed implementations. The main idea of our approach is to iteratively refine the model by adding new roles, resources, and sensitivity levels, while maintaining logical consistency and control over access policies. We used an abstract multidimensional matrix for the theoretical visualization of the refinement and the UPPAAL tool for developing and validating the models. Our approach is visualised using a healthcare case study, where hospital workflows are implemented.
In the modern world, efective management of business processes, particularly each workflow, directly
afects the success of the organization as a whole. A workflow is a sequence of tasks, actions, and
operations performed by roles within an enterprise to achieve set goals [
Traditional methods of manual analysis are no longer suficient for organizations due to the huge volume of data and tasks. Modeling of workflows have long been essential tools for studying the behavior of people, systems, and processes. This also applies to predicting performance and identifying bottlenecks. However, modeling workflows in actual conditions faces some problems. Modern approaches to business process management should take into account not only the need for formal modeling but also flexibility, adaptability, and the ability to utilize the latest technologies. The issue of access control within processes becomes especially critical, since the execution of operations is often associated with the processing of confidential information and interaction between roles with diferent levels of responsibility. Access control mechanisms in process models allow enterprises to improve the manageability and transparency of resource use and to minimize the risk of achieving strategic goals.
Designing reliable and manageable workflow systems requires a foundation in access control
modeling, layered architecture, and granularity. This paper uses a combination of several fundamental
approaches. The transition from an abstract model to specific access policies is carried out in a stepwise
manner using refinement [
In our previously proposed enterprise workflow modeling approach [
In this paper, we extend the previously proposed approach by introducing access control components
based on a hybrid RBAC and MAC approach. In this approach, roles not only structure the workflow
but also have specific permissions for operations (read, execute) on defined resources. Resources, in
turn, are classified by sensitivity levels. This extension enables providing the model with strict security
policies, especially when it comes to healthcare, space, and military industries [
We show the advantages of our method through a healthcare case study where medical staf, patients, and systems represent the roles. The approach is visualized using UPPAAL, and the models are available at the link.
Workflow modeling with access control in mind is rapidly evolving, integrating BPM, access control,
and formal methods [
Access control is the primary mechanism for ensuring information security. Its task is to limit the actions of subjects (user, system) over objects (data, resources) in working to achieve the goals of the enterprise. An efective access control system allows the prevention of unauthorized access and minimizes the risks of internal abuse. The choice of access control model critically afects the flexibility of management. The most used access control models are role-based and mandatory. In the context of large enterprise companies, role-based access control (RBAC) is most often used. Mandatory access control (MAC) is additionally used in the military, government, and healthcare sectors, where security is a high priority. Given that our case study is within the healthcare area, it is useful to consider both of these access control models.
Role-based access control (RBAC) is a standard mechanism for managing the access of users and systems
based on their role in an organization [
Mandatory Access Control (MAC) is an access control model where permissions are defined at the system level rather than at the user level. Restrictions are enforced by access policies and security labels. MAC does not use roles but strictly controls access through security levels.
Security level is a strictly defined characteristic of a subject that determines the category of data
to which the user has access. The security level is strictly fixed in the system and consists of two key
components: subject classification - the user’s clearance level, object classification - the security level of
the resource (class). Each resource is assigned a class, and each subject is assigned a clearance. Access
is allowed only if the subject’s clearance level is greater than or equal to the object’s sensitivity class
[
clearance() ≥ class() (1)
MAC and RBAC are role-based and label-based access control models, but each has its characteristics
and mechanisms for assigning rights, advantages, and limitations [
Based on this part of the analysis, we can conclude that in both cases, the user must have a label — a clearance level or role. In addition, MAC also protects objects that have sensitivity levels (classes). Here, we combine the two described models and obtain a hybrid flexible access model, where the role determines access, taking into account the type of sensitivity of objects and the level of access of each role.
As a result, our approach is based on the following: 1. Each user has a role. 2. The access level is assigned to the role rather than to an individual user. 3. Users may be granted diferent clearances despite having the same role. 4. Each object (or resource) has a sensitivity level (class). 5. Even if users have the same role and clearance, access to certain information may still be restricted based on resource sensitivity.
This is especially important in domains with critical information, such as healthcare, finance, and government systems. Based on this, access control matrices can be built by considering roles, resources, and sensitivity.
The simplest and most formal structure for representing access control is the Access Control Matrix
(ACM). The classic ACM is a two-dimensional table whose rows correspond to system subjects and
columns to objects. The matrix cells contain a set of permitted operations that a particular topic can
perform on the corresponding object (e.g., read, write, execute) [
The role-based workflow model is best modeled as a parallel system. Such a system comprises multiple
entities, including both people and systems or services, that interact simultaneously, independently,
and asynchronously. Given the high complexity of such systems, stepwise development is beneficial for
their formalization and synthesis. The proposed approach aims to gradually refine and verify the model,
improve manageability, and facilitate a stepwise transition by layers from an abstract representation
of the workflow to a specific model suitable for simulation of the process, taking into account the
synthesis of roles into a single, common workflow. The abstract model can be visualised using an
abstract access matrix with entities and their coordination. In the refinement of the model, this matrix
supports the synchronized development of roles, operations, resources, and sensitivity levels in a single
model. This approach provides an increased accuracy in access control and resource classification, as
well as detailed accounting of sensitivity levels, preserving the behaviour of the model. In addition, it
enables the implementation of the principle of least privilege, according to which a subject is granted
only the minimum rights necessary to perform their direct tasks [
Refinement [
At each refinement step, superposition refinement [
By discharging all these proof obligations for each refinement step in the system development, we have proven the correctness of the system concerning its specification. This means that the refined system should satisfy its invariant concerning the new behaviour, preserve the behaviour of the abstract system, and not introduce deadlocks, nor infinite loops that could suppress the old behaviour.
Stepwise superposition refinement can be seen as a layered development, where each refinement step
forms a separate layer that adds details on top of the abstract model [
Role refinement has been discussed in detail earlier [
Our approach allows us to form the model of access control as a matrix in order to visualize the
overall behavior of the workflow. This paper focuses only on internal roles, since they implement the
actions that make up the structure and sequence of steps in the workflow. Refinement is carried out in
layers from the abstract definition of roles to more specific ones, depending on the tasks performed.
Stepwise development of internal roles allows us to refine the workflow structure and to ensure the
correct inheritance of access rights. Clarifying roles at the initial stages ensures the level of importance
for compliance with the principles of least privilege (PoLP) [
Resources in the context of workflow are the objects on which operations are performed. They can be data, systems, services, or any other entities that roles interact with. Like roles, resources can be developed with superposition refinement, which is critical for ensuring the consistency of the access model.
In this paper, resource refinement is implemented as a stepwise refinement of an abstract resource into more specific ones. For example, resource "report" can be refined to be of attributes "financial" and "analytical". In addition, new resources can also be introduced in a refinement step. For instance, if at the abstract level the resource was represented only as a data source, then at the refinement step it can be introduced as a separate entity with new operations (e.g., execute) and included in the model as a new resource with access rights. This is considered as superposition and requires consistency with other dimensions (roles and security levels) of the model. Such an expansion of the resource set is driven by the functional requirements of the refined roles, which may require additional services or data to perform tasks. Therefore, resource refinement cannot be considered in isolation. It must be coordinated with other dimensions of the model.
New resources require correct classification by security level (sensitivity), as well as assignment of appropriate permitted operations within the refined access matrix. Sensitivity is a dimension related to access policy. The security level is stepwise refined into specific classes (e.g., sensitive is refined into confidential and secret). To ensure the correctness of the model and the consistency of all dimensions of the access matrix, the refined entities should satisfy the proof obligations in Section 4.1. Additionally, we introduced model development rules (see Fig. 1), which give guidelines for the development process. The combination of model development rules and proof obligations facilitates us to guarantee the correctness of the developed model. All entity refinements are reflected in a multi-dimensional access matrix. The result of stepwise development is a structured, formally refined model that is applicable both for simulating its behavior and for automatic synthesis of access policies. This is especially useful for systems where multiple roles perform actions on the same objects, but with diferent access rights.
In order for our approach to be more feasible, we need tool support. We use the UPPAAL tool [
We propose an approach to role-based enterprise workflow modeling driven by refinement and access
control. The scenarios take into account several aspects at once - role structure, resource hierarchy,
and levels of sensitivity and access. We build on our previous work [
Our approach contains four modeling stages. At the first stage, an internal role is defined, for which both a workflow model and an access control model will be developed. This article focuses on a hybrid access control model. Therefore, in addition to the role itself, it is necessary to determine the set of resources that are necessary to perform functional tasks and the minimum set of sensitivity levels that will limit access to confidential information.
The second stage involves stepwise construction of an abstract multidimensional access matrix (see Fig. 2). This structuring is the basis for unified access analysis. The matrix is a four-dimensional tensor with axes for roles, objects, role clearance, and object class. Each point in this multidimensional space represents a specific combination of a role interacting with a specific object, within a specific clearance level and sensitivity class. The abstract multidimensional access matrix can be formally represented as: : ( × ()) × ( × ()) → (2) where • – multiple roles (e.g., hospital staf); • () – clearances of roles (e.g., low, high, restricted); • – multiple objects or resources (data, systems); • () – classes of objects (e.g., public, confidential); • – the set of possible operations assigned to each admissible configuration.
The access conditions are checked for each configuration. According to the access rule, an operation is allowed if and only if the clearance of the role is higher than or equal to the class of the object. Operations are formed as a result of applying the access control policy to the combination of role, object, clearance, and class. Thus, the matrix describes not only the permitted combinations but also which operations are explicitly allowed in each context.
The main idea of our approach is to iteratively refine the model by adding new roles, resources, and security levels, while maintaining logical consistency and control over access policies. Relationships between roles in the modeling process are implemented through synchronization, which allows interactions between roles within a single workflow. After constructing the abstract matrix, the first layer of the model is developed and visualized in a verification tool (e.g., UPPAAL). Roles are given as templates, resources as states, and security levels as guards.
At the third stage, all components of the model are refined into more specific ones (Section 4): roles by grouping according to functions or responsibilities; resources by refining into new types or possibly adding new systems; security levels by strengthening them depending on roles and resources. Each refined entity is updated in the matrix, and changes in one dimension automatically afect other dimensions (cf. Fig. 2 and Fig. 3).
The fourth stage is the merging of the refined components and the creation of a refined access matrix (First layer) (see Fig. 3 as a pattern and the full refined version at the link.). The refined matrix is subsequently covered by the model at the next layer and verified accordingly. Comparison of the two layers allows us to assess how the refinement afects the security, consistency, and completeness of the model. This iterative structure makes our approach suitable for scalable enterprise architectures while ensuring controllability, formalization, and verifiability.
Our approach is visualised by a healthcare system, which is a complex environment in which various roles, data with diferent sensitivity levels, and strict operational constraints interact. The workflow model considers interaction between medical staf and patients, taking into account role diferences and data sensitivity. The process models hospital employees who act within clearly defined sub-roles and access levels corresponding to their authority. The patient is considered an auxiliary external role initiating the request process, while the main behavior of the system is modeled through the operations of internal roles. The goal of this work is to formally describe and stepwise refine the role-based workflow model, taking into account access rules based on data sensitivity. Hence, we formalize the behavior of roles and, on this basis, we visualize them and their interaction using the UPPAAL automata modeling tool, which allows us to simulate the workflow and verify it.
In the first stage of modeling, we develop an abstract layer. It includes one abstract role -
Hospital_Staf [
Thus, the matrix can be formally represented as a function: : ( × ) × ( × ) → {, } (3) where = {_ }, = { , , }, = {}, = {, }, and = {}.
At this stage, only one operation read is considered, since reading is the basic and most universal access operation. We chose read as a primary example, allowing us to test the logic of access control for the diferent values of clearance and class. The access policy is implemented according to the following logic: (read : permit) — if clearance is higher or the same as class, (read : deny) — if clearance is lower than class. Based on this, an abstract access matrix is developed and presented in Fig. 4 It displays all possible combinations of a role and its clearance level concerning resources of diferent sensitivity (class) for a fixed read operation. This matrix is the basis for defining guards in the UPPAAL model.
After constructing the matrix in Fig. 4, we proceed to modeling in UPPAAL. Roles, resources, and sensitivity levels are modeled as states, transitions, guards, and variables. In the abstract layer, the system is modeled as the interaction of three key entities: Patient, Hospital, and Hospital_staf. These entities are implemented as separate, independent templates in UPPAAL, which are synchronized via channels using variables to simulate the workflow in a hospital. The Hospital acts as a mediator that listens to all events of the roles. All its transitions are abstract and are implemented in Hospital_staf, where access levels are defined. The core logic is implemented in the Hospital_staf template, which models the role’s behavior and access to patient data. According to the access matrix (see Fig. 4), all six permissible combinations of the variables clearance and class were covered in the model. These variables are directly specified in the global declaration of the model: by default class and clearance are are of type int with the initial value 0, while permit and deny are of type bool and initialized to false. The sensitivity levels are encoded as integer constants with the following values: null = 0, undefined = 1, public = 2, and sensitive = 3.
Accordingly, the decision is made according to logic in Section 6.1 permit = true; if ≤ ∧ ̸= ∧ ̸= deny = true; if > ∧ ̸= ∧ ̸= (4) (5)
Thus, at each moment, the model covers a specific cell of the access matrix. The values of the variables are specified explicitly, and the simulation is performed for one fixed configuration, which afects the behavior of the entire system.
Initially, the patient arrives at the hospital, and their arrival is confirmed by a notification to the hospital(arrival_notification). This notification is the starting point for the medical staf workflow. The patient is moved to the state patient_in_progress. The hospital staf begins collecting the necessary data and measuring parameters, recording health indicators, and collecting additional data (data_collected). After completing the information collection, a decision is made on further verification and analysis of the data. At this stage, the hospital staf selects one of the possible scenarios for working with the collected information. The first option is manual verification, in which specialists independently analyse the collected parameters and decide on the patient’s further actions. If this option is selected, the staf manually verifies the data (data_checked_manually), after which the processing is completed.
The second possible option is to use the system with automated verification. If the hospital staf chooses to use the automated system (auto_data_check_requested), the data is sent to it for verification and analysis. Before the check of access, two key parameters are selected. The clearance is selected through one of three dedicated channels (hosp_staf_*_clearance), and class is set through a separate channel, depending on the type of information being processed (read_*_data). At this stage, the question of the availability of the system, including its tools, functions, and operations, arises. Since diferent roles of hospital staf imply diferent levels of permissions and capabilities, access to the system must be diferentiated. However, at an abstract level, we have defined only two possible access levels: access granted (permit) or access denied/no access (deny).
In case of access restriction (deny), the system blocks the use of its capabilities and redirects the hospital staf to manual checking. In this situation, the hospital staf is forced to analyze the data manually since automated tools are unavailable and cannot process the information. If access to the system is allowed (permit), the system continues processing the data.
Once all steps are completed, all temporary access parameters are reset (accesses_reseted). The patient processing is completed (process_finished), and the patient receives the status ready to leave the hospital (ready_to_leave). When the patient leaves the hospital (patient_left), the hospital confirms exit, and the arrival notification is reset (arrival_notification = false).
Although the presented abstract model provides a compact and correct representation of the access control logic, it includes only a single role (Hospital_Staf ) and resource (Data). Therefore, we apply stepwise refinement as described in Section 5. At the First refinement layer, the model is expanded by three dimensions: roles, resources, and security levels.
The abstract role Hospital_staf is refined into three new operational roles based on task: Registrar, Med_staf, and Physician. The Registrar is responsible for patient registration and admin data management. The Med_Staf performs basic medical procedures and preliminary evaluations, while the Physician examines the patient, establishes a diagnosis, and prescribes treatment.
The abstract resource Data was refined into two new sub-resources and one completely new resource, taking into account the source and usage of the data. A new resource Analyzer was added according to the superposition principle, which involves a new operation execute. Consequently, we received three new components of the model at Layer 1: Personal_data (patient data, e.g. name, gender, age, date of birth), Medical_data (patient medical parameters, e.g. tests, diagnoses, anamnesis), Analyzer (system for automated verification and analysis).
While personal data can be both public and sensitive, medical data is sensitive by default [
As a result of the refinement, the access control matrix is expanded (see Fig. 5) and now includes three new sub-roles, two new sub-resources, and a new resource, as well as a refined set of security levels. The new system Analyser is superposed on to the model by adding new channels, variables, and guards that perform new tasks in such a way that the old behavior of the model is not afected.
After the refinement, the template Hospital_Staf is refined into three separate templates corresponding to the refined roles Hospital _Staff ∈ {Registrator , Medical _Staff , Physician}. In the new model, each role performs its part of the process, initiating events, setting variables, and performing transitions when guards hold. Each of the new sub-roles now acts within new access levels, and operations on resources are permitted according to the updated First layer matrix (see Fig. 5). Interaction between roles is implemented through synchronization of the corresponding templates. Transitions between states occur when conditions (guards) hold and the values of variables are set by one role, and then read by another role. Data transfer between roles is organized independently and makes it possible to implement multithreading. Thus, the refined model preserves the integrity of the system. The refinement from the abstract level to the refined level can be proved correct, preserving the safety invariants.
The model is simulated separately for each refined layer, which allows for stepwise detection and correction of logical errors. At the abstract layer of the model, end-to-end scenarios were simulated to verify the overall access control logic. Scenarios can be executed manually, with stepwise tracking of all transitions and states, or automatically, using the Verifier module and pre-prepared scripts describing the expected behavior of the model. In addition to simulation, a formal check of the critical properties of the model is performed according to the formulas (4) and (5). In particular, the Deadlock-freeness (A[] not deadlock) is confirmed, as well as the reachability of correct execution branches depending on the configuration of input parameters. This checks that proof obligation 5 in Section 4.1 is satisfied.
The presented rules were implemented both in the abstract matrix and in a practical case study (see Fig. 6). This confirms that the proposed approach maintains logical integrity: roles are clarified without expanding rights, resources are fragmented or added only when needed, and security levels are strengthened depending on the context.
The proposed approach combines role structuring, matrix description of access logic, and stepwise refinement to formalize, simulate, and verify workflows in complex distributed systems. The refinement steps enable intuitive design of access control and formal validation. Unlike the classic RBAC model, where access is assumed to be based on a role, in the developed approach, access rights are refined and strengthened. A hybrid combination of RBAC and MAC allows for strict delimitation of access to sensitive data and the necessary flexibility for the daily work of the staf. This makes our approach relevant for medical and other sensitive domains. Using a multidimensional access matrix makes it possible to scale the model with minor efort since adding new roles, resources, or sensitivity levels does not require reworking the core logic. In addition, the approach allows for access refinement based on the context and level of data sensitivity. The proposed approach supports independent stepwise refinement of workflow components with their parallel execution. This creates a basis for modular development and stepwise validation of access policies, applicable both at the design and execution stages. Thus, the proposed approach provides a coherent transformation of an abstract description of access control policies to their executable and verifiable implementation, which makes it a promising tool for building reliable access control systems of high complexity and data criticality.
During the preparation of this work, the authors used Grammarly only for grammar and spelling checks and take full responsibility for the content.