Dynamic Transition Refinement

Refinement of Petri nets is well suited for the hierarchical design of system models. It is used to represent a model at different levels of abstraction.Usually, refinement is a static concept. For many scenarios, however, it is desirable to have a more flexible form of refinement. For example in the context of service updates, e.g. version control in distributed systems, a mechanism for dynamic transition refinement is needed.The requirement of dynamic refinement at runtime is quite strong. Since we would like to redefine the system structure by itself, transition refinement cannot be implemented by a model transformation. Instead, an approach is needed which allows for dynamic net structures that can evolve as an effect of transitions firing. In previous work we introduced nets-within-nets as a formalism for the dynamic refinement of tokens. Here we consider an extension of nets-within-nets that uses special net tokens describing the refinement structure of transitions. Using this formalism it is possible to update refinements, introduce alternative refinements, etc. We present some formal properties of the extended formalism and introduce an example implementation for the tool Renew in the context of workflow modeling.     

Verification of workflow nets with transition conditions

Workflow management is concerned with automated support for business processes.Workflow management systems are driven by process models specifying the tasks that need to be executed,the order in which they can be executed,which resources are authorised to perform which tasks,and data that is required for,and produced by,these tasks.As workflow instances may run over a sustained period of time,it is important that workflow specifications be checked before they are deployed.Workflow verification is usually concerned with control-flow dependencies only;however,transition conditions based on data may further restrict possible choices between tasks.In this paper we extend workflow nets where transitions have concrete conditions associated with them,called WTC-nets.We then demonstrate that we can determine which execution paths of a WTC-net that are possible according to the control-flow dependencies,are actually possible when considering the conditions based on data.Thus,we are able to more accurately determine at design time whether a workflow net with transition conditions is sound.     

P-F方法在工作流系统中的应用研究

P-F方法是作者正在进行的一项过程建模和过程改进的方法论研究,作为一种支持过程建模、控制和改进的方法,P-F方法同样可以应用于工作流系统中。P-F方法由概念模型和实施模型组成,概念模型包括Petrinet和形式化的PAB表,它可以应用于工作流的建模;P-F方法的复用机制支持工作流建模过程的复用;P-F引擎提供了工作流管理,并支持运行时的工作流模型的动态修改。论文在工作流和P-F方法的概念后,讨论了如何将P-F方法应用于工作流系统以及将P-F方法应用于工作流系统所带来的优点。     

Stabilization-Preserving Atomicity Refinement

Program refinements from an abstract to a concrete model empower designers to reason effectively in the abstract and architects to implement effectively in the concrete. For refinements to be useful, they must not only preserve functionality properties but also dependability properties. In this paper, we focus our attention on refinements that preserve the dependability property of stabilization. Specifically, we present a stabilization-preserving refinement of atomicity from an abstract model where a process can atomically access the state of all its neighbors and update its own state, to a concrete model where a process can only atomically access the state of any one of its neighbors or atomically update its own state. Our refinement is sound and complete with respect to the computations admitted by the abstract model, and induces linear step complexity and constant synchronization delay in the computations admitted by the concrete model. It is based on a bounded-space, stabilizing dining philosophers program in the concrete model. The program is readily extended to: (a) solve stabilization-preserving semantics refinement, (b) solve the stabilizing drinking philosophers problem, and (c) allow further refinement into a message-passing model.     

Structural soundness of workflow nets is decidable

The problem of deciding whether a given workflow net is k-sound for some k?1 is known as structural soundness. We prove that structural soundness of workflow nets is decidable.     

Completeness of fair ASM refinement

ASM refinements are verified using generalized forward simulations which allow us to refine m abstract operations to n concrete operations with arbitrary m and n. One main difference from data refinement is that ASM refinement considers infinite runs and termination. Since backward simulation does not preserve termination in general, the standard technique of adding history information to the concrete level is not applicable to get a completeness proof. The power set construction also adds infinite runs and is therefore not applicable either. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondeterminism to the initial state. Adding such prophecy information can be done not only on the semantic level, but also by a simple syntactic transformation that removes the choose construct of ASMs. The completeness proof is also translated to a completeness proof for IO automata. Finally, the proof is extended to deal with supplementary predicates, that specify fairness and liveness assumptions, by transferring a related result of Wim Hesselink for refinements that use the Abadi-Lamport setting.     

Verifying soundness of business processes: A decision process Petri nets approach

This paper presents a trajectory-tracking approach for verifying soundness of workflow/Petri nets represented by a decision-process Petri net. Well-formed business processes correspond to sound workflow nets. The advantage of this approach is its ability to represent the dynamic behavior of the business process. We show that the problem of finding an optimum trajectory for validation of well-formed business processes is solvable. To prove our statement we use the Lyapunov stability theory to tackle the soundness verification problem for decision-process Petri nets. As a result, applying Lyapunov theory, the well-formed verification (soundness) property is solved showing that the workflow net representation using decision process Petri nets is uniformly practically stable. It is important to note that in a complexity-theoretic sense checking the soundness property is computationally tractable, we calculate the computational complexity for solving the problem. We show the connection between workflow nets and partially ordered decision-process Petri net used for business process representation and analysis. Our computational experiment of supply chains demonstrate the viability of the modeling and solution approaches for solving computer science problems.     

Relational concurrent refinement part III: traces,partial relations and automata

Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-by-event basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational framework, eventwise verification methods for such refinement relations can be derived. In this paper, we continue our program of deriving simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension. We then extend our framework to include various notions of automata based refinement.     

Modal transition systems with weight intervals

We propose weighted modal transition systems, an extension to the well-studied specification formalism of modal transition systems that allows to express both required and optional behaviours of their intended implementations. In our extension we decorate each transition with a weight interval that indicates the range of concrete weight values available to the potential implementations. In this way resource constraints can be modelled using the modal approach. We focus on two problems. First, we study the question of existence/finding the largest common refinement for a number of finite deterministic specifications and we show PSPACE-completeness of this problem. By constructing the most general common refinement, we allow for a stepwise and iterative construction of a common implementation. Second, we study a logical characterisation of the formalism and show that a formula in a natural weight extension of the logic CTL is satisfied by a given modal specification if and only if it is satisfied by all its refinements. The weight extension is general enough to express different sorts of properties that we want our weights to satisfy.     

Bayesian hypothesis testing for pattern discrimination in brain decoding

Research in cognitive neuroscience and in brain–computer interfaces (BCI) is frequently concerned with finding evidence that a given brain area processes, or encodes, given stimuli. Experiments based on neuroimaging techniques consist of a stimulation protocol presented to a subject while his or her brain activity is being recorded. The question is then whether there is enough evidence of brain activity related to the stimuli within the recorded data. Finding a link between brain activity and stimuli has recently been proposed as a classification task, called brain decoding. A classifier that can accurately predict which stimuli were presented to the subject provides support for a positive answer to the question. However, it is only the answer for a given data set and the question still remains whether it is a general rule that will apply also to new data. In this paper we try to reliably answer the neuroscientific question about the presence of a significant link between brain activity and stimuli once we have the classification results. The proposed method is based on a Beta-Binomial model for the population of generalization errors of classifiers from multi-subject studies within the Bayesian hypothesis testing framework. We present an application on nine brain decoding investigations from a real functional magnetic resonance imaging (fMRI) experiment about the relation between mental calculation and eye movements.     

Towards the construction of workflow-suitable conceptual modelling techniques

Despite their high-level and graphical nature, workflow specifications require a significant amount of implementation detail — for example application programming interface, database access and programming mechanisms for information flow — for a more comprehensive validation than is currently possible. This is currently recognized as a deficiency in workflow conceptualization. Although conceptual modelling techniques are available which are expressive, comprehensive and precise enough, we believe, their concepts and features are not specialized enough for workflow domains. In this paper, we offer a comparative insight into techniques which characterize different aspects and approaches of workflow specifications. These are: structured process modelling, object-oriented modelling, behavioural process modelling and business-oriented modelling. In particular, we determine gaps for workflows capturing operational business transaction processing, for example those of insurance claims, bank loans and government-related registration. For technique construction, we describe five workflow suitability principles.     

Connectivity of workflow nets: the foundations of stepwise verification

Behavioral models capture operational principles of real-world or designed systems. Formally, each behavioral model defines the state space of a system, i.e., its states and the principles of state transitions. Such a model is the basis for analysis of the system’s properties. In practice, state spaces of systems are immense, which results in huge computational complexity for their analysis. Behavioral models are typically described as executable graphs, whose execution semantics encodes a state space. The structure theory of behavioral models studies the relations between the structure of a model and the properties of its state space. In this article, we use the connectivity property of graphs to achieve an efficient and extensive discovery of the compositional structure of behavioral models; behavioral models get stepwise decomposed into components with clear structural characteristics and inter-component relations. At each decomposition step, the discovered compositional structure of a model is used for reasoning on properties of the whole state space of the system. The approach is exemplified by means of a concrete behavioral model and verification criterion. That is, we analyze workflow nets, a well-established tool for modeling behavior of distributed systems, with respect to the soundness property, a basic correctness property of workflow nets. Stepwise verification allows the detection of violations of the soundness property by inspecting small portions of a model, thereby considerably reducing the amount of work to be done to perform soundness checks. Besides formal results, we also report on findings from applying our approach to an industry model collection.     

Comparing traditional conceptual modeling with ontology-driven conceptual modeling: An empirical study

This paper conducts an empirical study that explores the differences between adopting a traditional conceptual modeling (TCM) technique and an ontology-driven conceptual modeling (ODCM) technique with the objective to understand and identify in which modeling situations an ODCM technique can prove beneficial compared to a TCM technique. More specifically, we asked ourselves if there exist any meaningful differences in the resulting conceptual model and the effort spent to create such model between novice modelers trained in an ontology-driven conceptual modeling technique and novice modelers trained in a traditional conceptual modeling technique. To answer this question, we discuss previous empirical research efforts and distill these efforts into two hypotheses. Next, these hypotheses are tested in a rigorously developed experiment, where a total of 100 students from two different Universities participated. The findings of our empirical study confirm that there do exist meaningful differences between adopting the two techniques. We observed that novice modelers applying the ODCM technique arrived at higher quality models compared to novice modelers applying the TCM technique. More specifically, the results of the empirical study demonstrated that it is advantageous to apply an ODCM technique over an TCM when having to model the more challenging and advanced facets of a certain domain or scenario. Moreover, we also did not find any significant difference in effort between applying these two techniques. Finally, we specified our results in three findings that aim to clarify the obtained results.     

The Shadow Knows: Refinement and security in sequential programs

Stepwise refinement is a crucial conceptual tool for system development, encouraging program construction via a number of separate correctness-preserving stages which ideally can be understood in isolation. A crucial conceptual component of security is an adversary’s ignorance of concealed information. We suggest a novel method of combining these two ideas.Our suggestion is based on a mathematical definition of “ignorance-preserving” refinement that extends classical refinement by limiting an adversary’s access to concealed information: moving from specification to implementation should never increase that access. The novelty is the way we achieve this in the context of sequential programs.Specifically we give an operational model (and detailed justification for it), a basic sequential programming language and its operational semantics in that model, a “logic of ignorance” interpreted over the same model, then a program-logical semantics bringing those together — and finally we use the logic to establish, via refinement, the correctness of a real (though small) protocol: Rivest’s Oblivious Transfer. A previous report^? treated Chaum’s Dining Cryptographers similarly.In passing we solve the Refinement Paradox for sequential programs.     

Modeling and analysis of the behavior of information systems

Many widely used specification techniques for information systems are based on a hierarchy of information flow diagrams. A method is introduced which preserves the benefits of these techniques and adds the precision of the Petri net formalism. Information-flow diagram hierarchies are formalized by notions of net theory. The bottom-level nets of a hierarchy are treated as Petri nets. The behavior model of the information system is the Petri net derived by repeatedly replacing each part of a net by its associated refinement. As a prerequisite for such replacements, the data abstractions relation information flows of different level are specified by a semantic hierarchy data model. The nets in the hierarchy are appended by dynamic counterparts of the abstractions so that a consistent replacement becomes possible. The interface behavior of the nets in the hierarchy is analyzed, using the concept of behavior constraints as a formal measure of correct interface behavior. The behavior model can be derived in an iterative bottom-up way by first analyzing a net for fulfillment of its associated behavior constraint and afterward integrating it into the next-higher-level net     

基于工作流网的实时协同系统模拟技术

基于Petri网和工作流的概念，提出一种实时协同系统的形式化模拟与分析技术——逻辑工作流网，逻辑工作流网是抑制弧Petri网和高级Petri网的抽象和扩展，其变迁的输入／输出受逻辑表达式的约束，它与一般工作流网相比，能够在一定程度上缓解状态空间爆炸问题，且便于系统设计人员掌握和使用，该文分析了逻辑工作流网的若干性质及组合网的性质继承问题，并以网上企业销售系统为例，说明逻辑工作流网在实时协同系统模拟分析中的应用。     

Workflow performance analysis and simulation based on multidimensional workflow net

Workflow model performance analysis plays an important role in the research of workflow techniques and efficient implementation of workflow management. Instances dwelling times (IDT) which consist of waiting times and handle times in a workflow model is a key performance analysis goal. In a workflow model the instances which act as customers and the resources which act as servers form a queuing network. Multidimensional workflow net (MWF-net) includes multiple timing workflow nets (TWF-nets) and the organization and resource information. This paper uses queuing theory and MWF-net to discuss mean value and probability distribution density function (PDDF) of IDT. It is assumed that the instances arrive with exponentially distributed inter-arrival times and the resources handle instances within exponentially distributed times or within constant times. First of all, the mean value and PDDF of IDT in each activity is calculated. Then the mean value and PDDF of IDT in each control structure of a workflow model is computed. According to the above results a method is proposed for computing the mean value and PDDF of IDT in a workflow model. Finally an example is used to show that the proposed method can be effectively utilized in practice.     

Model checking multi-agent systems with logic based Petri nets

We introduce a class of Petri nets, simple logic Petri nets (SLPN), that are based on logical expressions. We show how this type of nets can be efficiently mapped into logic programs with negation: the corresponding answer sets describe interleaved executions of the underlying nets (Theorem 1). The absence of an answer set indicates a deadlock situation. We also show how to correctly model and specify AgentSpeak agents and multi-agent systems with SLPN’s (Theorem 2). Both theorems allow us to solve the task of model checking AgentSpeak multi-agent systems by computing answer sets of the obtained logic program with any ASP system.     

On generating ⁎-sound nets with substitution

We present a method for hierarchically generating sound workflow nets by substitution of nets with multiple inputs and outputs. We show that this method is correct and generalizes the class of nets generated by other hierarchical approaches. The method involves a new notion of soundness which is preserved by the generalized type of substitution that is presented in this paper. We show that this notion is better suited than ⁎-soundness for use with the presented type of generalized substitution, since ⁎-soundness is not preserved by it. It is moreover shown that it is in some sense the optimal notion of soundness for the purpose of generating sound nets by the presented type of substitution.     

A tactic language for refinement of state-rich concurrent specifications

Circus is a refinement language in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but since refinements may be long and repetitive, the practical application of this technique can be hard. Useful strategies have been identified, described, and used, and by documenting them as tactics, they can be expressed and repeatedly applied as single transformation rules. Here, we present ArcAngelC, a language for defining such tactics; we present the language, its semantics, and its application in the formalisation of an existing strategy for verification of Ada implementations of control systems specified by Simulink diagrams. We also discuss its mechanisation in a theorem prover, ProofPower-Z.