Test-driven declarative process modelling combines process models with test traces and has been introduced as a means to achieve both the flexibility provided by the declarative approach and the comprehensibility of the imperative approach. Open test-driven modelling adds a notion of context to tests, specifying the activities of concern in the model, and has been introduced as a means to support both iterative test-driven modelling, where the model can be extended without having to change all tests, and unit testing, where tests can define desired properties of parts of the process without needing to reason about the details of the whole process. The openness however makes checking a test more demanding, since actions outside the context are allowed at any point in the test execution and therefore many different traces may validate or invalidate an open test. In this paper we combine previously developed static techniques for effective open test-driven modelling for Dynamic Condition Response Graphs with a novel efficient implementation of dynamic checking of open tests based on alignment checking. We illustrate the static techniques on an example based on a real-life cross-organizational case management system and benchmark the dynamic checking on models and tests of varying size.

Most contemporary process discovery methods take as inputs only positive examples of process executions, and so they are one-class classification algorithms. However, we have found negative examples to also be available in industry, hence we build on earlier work that treats process discovery as a binary classification problem. This approach opens the door to many well-established methods and metrics from machine learning, in particular to improve the distinction between what should and should not be allowed by the output model. Concretely, we (1) present a verified formalisation of process discovery as a binary classification problem; (2) provide cases with negative examples from industry, including real-life logs; (3) propose the Rejection Miner binary classification procedure, applicable to any process notation that has a suitable syntactic composition operator; (4) implement two concrete binary miners, one outputting Declare patterns, the other Dynamic Condition Response (DCR) graphs; and (5) apply these miners to real world and synthetic logs obtained from our industry partners and the process discovery contest, showing increased output model quality in terms of accuracy and model size.

We present an approach to the proactive enforcement of provisions and obligations, suitable for building policy enforcement mechanisms that both prevent and cause system actions. Our approach encompasses abstract requirements for proactive policy enforcement, a system model describing how enforcement mechanisms interact with and control target systems, and concrete policy languages and associated enforcement mechanisms. As examples of policy languages, we consider finite automata and timed dynamic condition response (DCR) graphs. We use finite automata to illustrate the basic principles and DCR graphs to show how these principles can be adapted to a practical, real-time policy language. In both cases, we show how to algorithmically determine whether a given policy is enforceable and, when this is the case, construct an associated enforcement mechanism. Our approach improves upon existing formalisms in two ways: (1) we exploit the target system’s existing functionality to avert policy violations proactively, rather than compensate for them reactively; and (2) rather than requiring the manual specification of remedial actions in the policy, we deduce required actions directly from the policy.

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 study non-equivocation in synchronous agreement protocols: the restriction on faulty processes that they cannot act differently towards distinct non-faulty processes. Guarantees of non-equivocation have been used to provide improved fault tolerance in agreement protocols, and various mechanisms for achieving it have been proposed. However, the exact meaning of non-equivocation varies subtly in the literature. In this paper, we propose two different formal notions of non-equivocation: strong and weak. We define both as fault models for synchronous agreement protocols with reliable channels, and we show how the two models yield distinct bounds for the minimal number of communication rounds required and the maximum number of faulty processes tolerable to achieve agreement: 1 round, n > t for strong non-equivocation; and t + 1 rounds, n > 2t for weak non-equivocation. This makes weak non-equivocation the only fault model with a lower bound on fault tolerance of n > 2t for broadcast agreement and interactive consistency, confirming the folklore knowledge that equivocation is, in a sense, the most critical of the Byzantine faults. Finally, we show how the weak and strong non-equivocation fault models relate to well-known agreement problems: strong non-equivocation corresponds to Byzantine broadcast and weak non-equivocation to crusader agreement.

Enterprise computing applications generally consists of several inter-related business processes linked together via shared data objects and events. We address the open challenge of providing formal modelling and implementation techniques for such enterprise computing applications, introducing the declarative, data-centric and event-driven process language RESEDA for REactive SEmi-structured DAta. The language is inspired by the computational model of spreadsheets and recent advances in declarative business process modelling notations. The key idea is to associate either input events or reactive computation events to the individual elements of semi-structured data and declare reactive behaviour as explicit reaction rules and constraints between these events. Moreover, RESEDA comes with a formal operational semantics given as rewrite rules supporting both formal analysis and persistent execution of the application as sequences of rewrites of the data. The data, along with the set of constraints, thereby at the same time constitutes the specification of the data, its behaviour and the run-time execution component. This key contribution of the paper is to introduce the RESEDA language, its formal execution semantics and give a sufficient condition for liveness of programs. We also establish Turing-equivalence of the language independently of the choice of underlying data expressions and exemplify the use of RESEDA by a running example of an online store. A prototype implementation of RESEDA and the examples of the paper are available on-line at http://dcr.tools/reseda.

We present a system model, an enforcement mechanism, and a policy language for the proactive enforcement of timed provisions and obligations. Our approach improves upon existing formalisms in two ways: (1) we exploit the target system's existing functionality to avert policy violations proactively, rather than compensate for them reactively, and, (2) instead of requiring the manual specification of remedial actions in the policy, we automatically deduce required actions directly from the policy. As a policy language, we employ timed dynamic condition response (DCR) processes. DCR primitives declaratively express timed provisions and obligations as causal relationships between events, and DCR states explicitly represent pending obligations. As key technical results, we show that enforceability of DCR policies is decidable, we give a sufficient polynomial time verifiable condition for a policy to be enforceable, and we give an algorithm for determining from a DCR state a sequence of actions that discharge impending obligations.

We implement strength reduction and loop-invariant code motion by specializing instrumented interpreters; we define a novel program transformation that uses bisimulation to identify and remove code duplication in residual programs; and we discover that some simple classical optimizations, notably constant-propagation, seemingly do not lend themselves to implementation by specialization of instrumented interpreters.