Keywords

1 Introduction

Virtual factories (vF) arise out of the amalgamation of distributed manufacturing, virtual enterprises, and business management. A vF describes a distributed and integrated computer-based model simulating total manufacturing environment. It incorporates all the tasks and resources necessary to accomplish the operation of designing, producing and delivering a product [1, 2]. From the manufacturing practice, the machines, processes, related products and services are directly made compatible to support automated design and verification of collaborative business processes (cBP). Individual enterprise business processes integrate into a cBP jointly designed and implemented. The pool of skills, resources and technology is exploited to support the analysis of different design alternatives, performance evaluation and reduced time-to-production.

cBPs are complex; they are dynamic, cross organizational boundaries and rely on data from partners for their design and execution. They differ from single organization business processes (sBP) in nature and structural design [3, 4] more so in virtual environments where execution is automated. It is resonant therefore to verify cBPs before their implementation to avoid errors at execution. We posit that verification should be supported with canonical approaches. Literature is scanty concerning approaches and tools applicable to verify cBP models especially for vF yet sBP verification has been well addressed with various approaches [3, 5,6,7,8,9, 10, 11]. However, these approaches present realizable knowledge gaps; they concentrate on control flow aspects [3, 4, 9,10,11,12, 14, 15] and abstract from other perspectives like data which is a major input for smart devices and machines in a vF. Besides, best practice linking verification approaches to vF cBPs is missing. The EU H2020 FIRST project aims to develop a method to support non expert end users to model and verify vF cBPs.

This paper presents the state of art in business process verification approaches and makes a comparative assessment of their fitness to verify vF cBPs. The vF cBPs being data intensive, we describe their requirements and how to support their verification in a vF environment. The rest of the paper is structured as follows; Sect. 2 presents the requirements for cBP verification by describing their characteristics in a vF setting, Sect. 3 presents the state-of-art in process verification. In Sect. 4 we present a framework of cBP verification while Sect. 5 discusses the related work. We make conclusions and outlook for future work in Sect. 6.

2 Requirements of CBP Model Verification

For us to support cBP verification, it is objective to understand their nature and requirements. We postulate that cBPs should conform to a set of requirements described below:

Span different organisations: Collaboration involves different partners working together for a common goal. In terms of business process management the partners jointly define business and technical solutions. The business solution describes partner behavior in the cBP while the technical solution defines the specifications and implementation of the supporting system [16]. The approach to verify such processes should consider the diversity of users, their roles and the distributed nature of the cBP.

Communication/Interaction Protocol: Typical of the cBP are the forms of communications and interactions expressed as message exchanges among partners who engage in discussions before reaching a decision. cBPs require dedicated interaction protocols through which partners can communicate. Various interaction protocols are proposed [4, 17] but they do not pass the criteria to support cBP verification.

Dynamism, Flexibility and Complexity: CBPs may be composed from services offered by partners using Service oriented architecture. The partners timelessly and continuously push in changes that impact on the process outcome. Such volatility should be taken care or at design time through verification to prevent execution flaws and support change integration, propagation and continuous verification.

Data requirements: cBP data requirements relate to several issues to support operations and analytics for decision making. Workflow systems embraced 2 kinds of data i.e. control data (for routing purposes) and production data (information objects like documents, forms, and tables) [8]. For the smart factory data is exploited by the cyber physical systems, internet of things and cloud computing to support operations by autonomously exchanging information, triggering actions and controlling operations. Factory automation relies on intelligent data gathering and exchange between the systems. Verification should cater for data requirements and data patterns to support analytics for decision making and driving operations at the factory floor. A verification tool should be able to support verification of such requirements.

The following section presents the state of art in business process verification by discussing how existing approaches and tools compare in regard to supporting cBP model verification given the suggested requirements.

3 State of the Art in Business Process Verification

3.1 Business Process Verification Approaches

Business process verification as a concept of model checking (MC) has various applications; i.e. Variability - checking to ascertain how business processes vary in behavior over a set of conditions [12, 18]. Compliance - model conformance with requirements, laws or standards [13,14,15, 19,20,21]. Compatibility - aligning partner processes to the choreography i.e. the interaction architecture through which the cBP is executed [18, 22]. Verification – checking models to correct errors. During business process design, more time is spent on verification than actual design. Formal verification leads to seminal advantages as described in [19, 23].

Various verification approaches exist along with supporting tools. This section presents a description of some of the most commonly applied verification approaches and tools in literature. The tools are broadly categorized according to the technique or language on which they are semantically based .i.e. Petri nets and Temporal Logic. Petri nets describe a bipartite directed graph with two nodes i.e. Places (circles) and Transitions (rectangles) [24] connected by directed arcs. Petri nets are applied in workflows to create Workflow Nets. A workflow net must meet a syntactical requirement of having each place or transition on a direct path from start to end. Such requirement satisfies the workflow property of soundness [3, 11, 25, 26]. For details on petri nets and workflow verification the reader is referred to [6]. Classical petri nets become very large, inaccessible and difficult to interpret [3]. The color petri nets solve the limitations. A discussion of some of the most common petri net based tools follows;

Colored Petri Nets (CPN Tools); support modelling of data, objects and structures using color [27] and support verification [28, 29]. Color expresses each instance as unique in a case, time captures time related information to track capacity of a process, and hierarchy supports hierarchical design of process models and sub models. CPN tools integrate with other tools to support verification of models, for instance Protos and E-C-A [29].

Yet Another Workflow Language (YAWL); it is both a workflow modelling and verification tool based on the Petri nets [25] and workflow patterns [30]. It provides a graphical editor enhanced with built-in verification functionality supporting early time detection of model errors. It provides support for verification based on Reset nets and transition invariants (WofYAWL editor plug-in) [31]

Protos: Protos supports process model definition and analysis based on different perspectives of data and control flow. It supports simulation of models before their enactment and execution. Protos2CPN tool is an integration of Protos with CPN tools to support process model verification [29].

FlowMake: The tool supports design time identification of errors in models before implementation in WFMS [32]. Graph reduction algorithm [33] is employed to verify workflows for syntactic correctness by identifying and eliminating structural conflicts like deadlocks and lack of synchronization. Correct structures are removed until the WF graph remains empty through a conflict reserving reduction process.

Application Development based on Encapsulated pre-modelled Process Templates (ADEPT)/AristaFlow; a family of tools used to support modelling and verification of flexible and dynamic business processes [34,35,36,37]. Based on clinical business scenarios, ADEPT enables process implementers, application developers and end users to model and verify models through its features like; extended graphical interfaces, on-the-fly correctness checks [37], process templates and structural transformation of processes. It supports for ad-hoc changes and their propagation.

The tools described from this point are based on Temporal Logic formalism. Temporal Logic supports ways to specify systems and check models for correctness against a set of properties expressed in form of event orderings in time [20, 38]. It is widely applied to verify concurrent systems, distributed systems, context aware and collaborative systems. For details on temporal logic and its various branches and application the reader is referred [39].

Declarative Service Flow Language (DecSerFlow): DecSerFlow supports specification, enactment, and monitoring of service flows in a declarative nature. Verification of service workflow conformance is achieved by subjecting models to temporal logic constraints enforced by the engine and guarded against their violations. The engine monitors the violations as well [11, 14].

HYbrid TECHnology (HyTech); supports automatic verification of system models against properties specifications expressed in real time temporal logic through symbolic computation [7]. Models are verified for reachability, liveness, time boundedness and duration properties [40]. HyTECH is recommended for verification of mission critical systems. However, the tool is limited to verification of small systems [41] and linear hybrid systems [42]. Some of the limitations have been overcome by HyTECH+ tool [42] which is an extension to the classical HyTECH.

Symbolic Model Verifier (SMV); operates like HyTECH to exhaustively verify models and provide counter examples. It is limited by state explosion. NuSMV is a modified version to verify synchronous finite-state and infinite-state systems [43, 44].

SPIN; supports verification of asynchronous systems by verifying for correctness. The properties are expressed as standard temporal logic while model specifications as a Buchi automaton. The Buchi automaton is a product from computation of the claims and the automaton representing the global state space. The product is then checked, if empty then the claims are not satisfied for a given system, otherwise it contains the behavior that satisfies the original temporal formula. To limit state explosion, partial order reduction method is employed [25, 45,46,47]. However state explosion remain a challenge limiting applicability to verify cBP model.

KRONOS; applies timed automata and timed temporal logic to verify models for reachability properties [48, 49] like; safety (system never enter unsafe states), non zenoness (the state of the system does not prevent time to diverge) and bounded response (ability to respond to requests issued in specified time)

UPPAAL; supports on-the-fly verification of real time systems modelled as timed automata with extended data. It checks models for reachability and invariability properties with support for diagnostic trace [5, 50, 51]. State explosion remains a challenge limiting its application to cBP model verification. Table 1 presents a summary of the tools and the related properties that they verify in business process models.

Table 1. Showing summary of tools and properties
Full size table

3.2 Limitations of the Verification Approaches to Verify cBP Models

Based on the assessment in Table 1, we find verification approaches lacking in terms of the support they accord to users to verify cBPs. We expound on these limitations; Support sBP verification; existing approaches were developed to support modelling and simulation of single organization business processes, not cBPs. Simulation is not an exhaustive way to verify models since it is based on assumptions that may deviate from actual. Some tools integrate with other tools to support verification (e.g Protos and E-C-A integrate with CPN tools) [29] while others like YAWL verify models modelled in the same language. Woflan was created as an independent verification tool to verify models developed in Staffware, COSA and MQ [52]. These tools remain limited for vF cBP verification.

The semantical and architectural structure: The tools do not support the semantical structure and architectural requirements for cBP verification i.e. the lack of interfaces or open structures to permit integration with other systems manifests their inability to support collaborative environments. YAWL avails web based plugins for integration with other systems but support for simultaneous model and sub models verification is limited. Additionally the semantical structure of other tools is ambiguous and a source of semantical errors and conflicts when models are merged for verification [53].

Support for data and data analytics: Most approaches target verification based on control flow perspective and abstract from other perspectives like data, resources, tasks and applications [6, 8, 9, 16, 52]. The justification advanced for abstraction never anticipated future data requirements that vF processes currently present. The smart factory heavily relies on data routed between interconnected smart devices to drive the automated machines at the factory floor. Moreover, data is used to support analytics for other seminal benefits like decision making, projections and future planning. Therefore during verification data and data analytics should be supported at both design time and runtime.

4 Framework for Assessing CBP Model Verification Approaches

4.1 Assessment Criteria

Language comparisons are based on different factors that may be objective or subjective [53]. A set of parameters to compose our criteria intended to assess the inherent traction and precision of the verification approaches and their appropriateness to verify vF cBP models. The following section briefly describes these parameters;

Expressibility; assesses the degree to which an approach can represent any number of models in different application domains [54, 55]. In [33], the expressive power of a modelling technique was gauged in terms of its capability to represent specific process requirements. In our case, we consider expressiveness of a model verification tool in terms of the degree to which it supports one to verify different properties of cBP models given their specifications.

Flexibility; describes the ability to support exception handling, possibility to make changes at design time or runtime, and support for scalability especially as the cBPs evolve and grow.

Suitability; describes the appropriateness of a tool to a particular application domain [5, 54]. In our case we assess suitability in terms of the degree to which a tool is applicable to verify vF cBP models given their structure and architecture for instance; verify semantical correctness of main models and sub models simultaneously.

Complexity and Limitations; assesse the level of difficulty an approach presents to work with [33] or its features that make it easy to work with while being used to verify process models. The limitations refer to the different forms of inadequacies of a tool that render it inappropriate and inapplicable to verify vF collaborative business process models.

4.2 Application of the Assessment Framework

This section presents the application of the assessment framework criteria to assess the existing verifications approaches and tools. A summary of this assessment is presented in Table 2 after which we discuss the assessment results in the section that follows after;

Table 2. Showing a Comparative assessment of the verification tools
Full size table

Assessment based on the proposed criteria as summarized in Table 2 and in reference to Table 1 reveals various properties being checked by the existing tools. However, these properties are expressed in relation to single organization business processes. The interpretation and connotation of these properties may not be the same for cBPs: for instance having sound models for a single organization business process does not guarantee their soundness in a collaborative environment. Furthermore verifying for reachability, safeness, liveness and boundedness in a single organization process is not as complex as verifying the same properties for cBPs where the requirements differ. Moreover, there is no silver bullet solution; no single approach verifies all necessary properties for all situations. For example Petri net based tools like YAWL, Woflan, and CPN are lacking in terms of time based requirements for models. Temporal logic based tools like SPIN, KRONOS and HyTECH suffer from state explosion problem that limits the number and size of models that can be checked. Besides, the counter examples they provide on discovery of errors remain difficulty to understand for the ordinary users. Above of all, the inability and inconsideration for data perspective leaves them inappropriate to verify cBPs that are highly data intensive. In summary, using the parameters in the proposed criteria we note the following in view of cBPs;

Expressiveness - most approaches are not specific to a particular application domain but incapable of representing as many models for interacting enterprises as may be required. To that effect such approaches would not verify the structure, data and execution requirements of cBPs.

Flexibility - besides HyTECH, UPPAAL and Woflan, all other tools reviewed have the capability for exception handling, permitting ad hoc changes and scalability. Such attributes meet the requirements of cBPs that are highly variable and dynamic due to the diversity of process owners and environment in which they apply. However the tools verify already completely designed models. This renders them rigid and inflexible for application to cBPs [17].

Suitability - the techniques are inappropriate and not suitable for verification of vF cBP models. The tools support single model verification at a time which makes it difficult for cBPs that are composed of many sub models that are merged for verification. Lack of standardized semantics introduces semantical errors when models to be verified are developed from different tools. This further limits the application of these tools to vF cBP verification.

Complexity\ Limitations - most tools present graphical user interfaces making them easy for the non-expert users to apply. Moreover, temporal logic based tools provide counter examples where model errors exist. However, the provided counter examples are not a guarantee for correctness of the model. Besides, temporal logic expressions remain complex for non-expert users in the collaborative environments [40].

5 Related Work

This section presents work related to our study but we are keen to highlight how our work differs.

In [33] a survey of comparative business process modelling approaches is presented based on graph based vs rule based approaches. The comparison criteria included parameters like expressibility, flexibility, adaptability, dynamism and complexity, and an analysis of how the approaches score was presented. The work is presented under the umbrella of process modelling while ours is based on supporting cBP model verification in a vF environment. In [23], a survey of formal verification approaches for business process diagrams is presented and compared with respect to motivation behind their development i.e. the aim of verification, method of formalization and logics. This survey was based on verification of single organization business process models where our work concentrates on assessment of approaches that support cBP verification. Moreover they do not assess the tools based on their application or competency but rather on what motivated their developers. In our study the assessment is based on how well the approaches can support verification in a collaborative environment.

Further work by [56] presents an analysis of verification tools based on the forms and application of verification by categorizing it into variability, compliance and compatibility. The approaches are then discussed and compared under the same breadth. Our work differs in a way that we propose and present an assessment framework to analyze verification tools based on their traction, precision and competency to verify cBP in vF environment.

6 Conclusion and Future Work

Verification is a way to ensure error free business process models at execution time. The existing research reveals various efforts towards business process modelling and verification in form of theories, approaches, tools and methodologies but realizable knowledge gaps exist. Verification of single organization business processes is well addressed in literature but work remains at large concerning techniques and tools specific for verification of cBP models more so for vF environments. The nature of cBPs in vF relies on data to enable real-time actionable intelligence. Supporting data analytics presents the potential to increase productivity, undertake preventive maintenance through projected breakdowns and generate cost savings. Recommendation for a verification method specific to cBP models in a vF environment is appropriate to meet the expressiveness, flexibility, suitability and complexity required in such environment given its requirements as discussed above.