Context: Process compliance refers to the alignment between business processes and regulatory requirements. Compliance is challenging because it requires expressing the intent and possible interpretations of laws into formal models, aligning models with foreseeable executions, and inspecting whether these executions could generate violations. While business process compliance has been studied through conformance checking techniques, most regulatory requirements are defined in subjective and high-level terms, limiting the application of rule- and alignment-checking algorithms to restricted cases where requirements are formally specified. Objective: This paper investigates how compliance can be assessed against high-level and non-functional requirements rather than low-level process events. We aim to raise the abstraction level of compliance checking from specific task execution to the satisfaction of high-level business goals and subjective qualities. Method: We propose a framework that links process models with goal models to capture functional decomposition, non-functional requirements, and contribution links, developed iteratively with legal practitioners. Business processes (imperative and declarative) are represented as labeled transition systems (LTS), while goals and qualities are modeled using iStar models. A mapping function synchronizes process activities with goal elements. Compliance is then checked through state reachability, where all qualities are satisfied, with computational support from the Kogi tool. We refine compliance into weak, strong, and monotonic quality satisfaction, also called stability. Results: From a technical view, the framework has demonstrated expressiveness, feasibility, and modularity by distinguishing strong, weak, and monotonic compliance. From a legal perspective, it has shown potential to enhance transparency in evidence-based decision-making and supports the traceability of knowledge bases underpinning system development, as illustrated by the use case from Regulation EC 261/2004. Conclusions: The proposed approach enables compliance checking against high-level and non-functional requirements, showing potential to distinguish among compliant behaviors and increase goal satisfaction traceability compared to rule-based conformance methods.

Business process management employs process models and event logs to represent the behavior of the information systems under study. Traditional case-centric notions consider the order of activities and events in isolated process instances. The emerging field of object-centric processes challenges this assumption by putting objects in the center. Object-centric process mining and modeling approaches identify the structure of co-evolving data objects that influence the behavior of an information system to provide a comprehensive view of the system behavior. Object-centricity has been investigated independently in process modeling and in process mining, which resulted in the coexistence of seemingly contradictory assumptions and definitions. As a community effort, this research manifesto relates and aligns existing terminologies, definitions, and perspectives to provide a common ground for current and future research in object-centric business process management. Based on the current state of research, we propose a conceptualization that sets process models and event logs in relation to the information system’s behavior and the execution data it generates. The conceptualization aims at aligning different terminologies and, thus, providing a basis to model and analyze behavioral characteristics. Building on this common ground, we identify open research challenges along the most relevant research areas in object-centric process management. For each research area, its current status is investigated and an outline of the most relevant research challenges is presented.

Abstract Session-based concurrencyis a type-based approach to the analysis of message-passing programs. These programs may be specified in anoperationalordeclarativestyle: the former defines how interactions are properly structured; the latter defines governing conditions for correct interactions. In this paper, we study rigorous relationships between operational and declarative models of session-based concurrency. We develop a correct encoding of session $$\pi $$ π -calculus processes into the linear concurrent constraint calculus ( $$\texttt {lcc}$$ lcc ), a declarative model of concurrency based on partial information (constraints). We exploit session types to ensure that our encoding satisfies precise correctness properties and that it offers a sound basis on which operational and declarative requirements can be jointly specified and reasoned about. We demonstrate the applicability of our results by using our encoding in the specification of realistic communication patterns with time and contextual information.

We presentParTypes, a type discipline for parallel programs. The model we have in mind comprises a fixed number of processes running in parallel and communicating via collective operations or point-to-point synchronous message exchanges. A type describes a protocol to be followed by each processes in a given program. We present the type theory, a core imperative programming language and its operational semantics, and prove that type checking is decidable (up to decidability of semantic entailment) and that well-typed programs do not deadlock and always terminate. The article is accompanied by a large number of examples drawn from the literature on parallel programming.

Legal compliance is an important part of certifying the correct behaviour of a business process. To be compliant, organizations might hard-wire regulations into processes, limiting the discretion that workers have when choosing what activities should be executed in a case. Worse, hard-wired compliant processes are difficult to change when laws change, and this occurs very often. This paper proposes a model-driven approach to process compliance and combines a) reference models from laws, and b) business process models. Both reference and process models are expressed in a declarative process language, The Dynamic Condition Response (DCR) graphs. They are subject to testing and verification, allowing law practitioners to check consistency against the intent of the law. Compliance checking is a combination of alignments between events in laws and events in a process model. In this way, a reference model can be used to check different process variants. Moreover, changes in the reference model due to law changes do not necessarily invalidate existing processes, allowing their reuse and adaptation. We exemplify the framework via the alignment of laws and business rules and a real contract change management process, Finally, we show how compliance checking for declarative processes is decidable, and provide a polynomial time approximation that contrasts NP complexity algorithms used in compliance checking for imperative business processes. All-together, this paper presents technical and methodological steps that are being used by legal practitioners in municipal governments in their efforts towards digitalization of work practices in the public sector.

We report on a new approach to co-creating adaptive case management systems jointly with end-users, developed in the context of the Effective co-created and compliant adaptive case Management Systems for Knowledge Workers (EcoKnow.org) research project. The approach is based on knowledge from prior ethnographic field studies and research in the declarative Dynamic Condition Response (DCR) technology for model-driven design of case management systems. The approach was tested in an operational environment jointly with the danish municipality of Syddjurs by conducting a service-design project and implementing an open source case manager tool and a new highlighter tool for mapping between textual specifications and the DCR notation. The design method and technologies were evaluated by understandability studies with end-users. The study showed that the development could be done in just 6 months, and that the new highlighter tool in combination with the traditional design and simulation tools, supports domain experts formalise and provide traceability between their interpretations of textual specifications and the formal models.

We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution.

Session-based concurrency is a type-based approach to the analysis of communication-intensive systems. Correct behavior in these systems may be specified in an operational or declarative style: the former defines how interactions are structured; the latter defines governing conditions. In this paper, we investigate the relationship between operational and declarative models of session-based concurrency. We propose two interpretations of session π-calculus processes as declarative processes in linear concurrent constraint programming (lcc). They offer a basis on which both operational and declarative requirements can be specified and reasoned about. By coupling our interpretations with a type system for lcc, we obtain robust declarative encodings of π-calculus mobility.