http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
A Place-Invariant Based Method for Supervisory Control of Workflow Nets
Shingo Yamaguchi,Soichiro Nagano 대한전자공학회 2015 ITC-CSCC :International Technical Conference on Ci Vol.2015 No.6
In this paper, we proposed a supervisory control method for workflow nets. Workflow nets are a particular class of Petri nets, but have analysis techniques for more properties, e.g. logical correctness called soundness, than Petri nets. We tackled the following problem: Given a (plant) workflow net (NP ;M0P ) and a constraint specification, construct a workflow net (NS;M0S) which consists of NP and a (supervisory controller) Petri net NC which satisfies the constraint specification. We proposed (i) a sufficient condition for the existence of (NS;M0S) based on place-invariants, and (ii) a procedure to construct (NS;M0S). The advantage of our method is to enable us to take account of logical correctness which may be lost by supervisory control. We also illustrated the proposed method with an application example and showed its usefulness.
Two Step Framework to Extend Workflow Nets and Soundizability Problem
Shingo Yamaguchi,Ryo Ikeda,Minoru Tanaka 대한전자공학회 2009 ITC-CSCC :International Technical Conference on Ci Vol.2009 No.7
We discuss in this paper whether we can extend work-flow nets (WF-nets for short) under the condition to preserve behavioral inheritance and soundness. We propose a two step framework to extend WF-nets, i.e. we first extend a given WF-net under the condition to preserve only behavioral inheritance, and then correct it to be sound if necessary. We tackle a problem of deciding whether we can correct an unsound WF-net to be sound under the condition to preserve behavioral inheritance, named soundizability problem. There are two kinds of behavioral inheritance: Projection inheritance and protocol inheritance. Our results show that if an acyclic free choice WF-net is extended under the condition to preserve projection inheritance, the extended WF-net is sound; If an acyclic free choice WF-net is extended under the condition to preserve protocol inheritance, the extended WF-net may be unsound; The unsound extended WF-net cannot be corrected to be sound under the condition to preserve projection inheritance, but may be corrected under the condition to preserve protocol inheritance.
On Verification and Application of Behavioral Inheritance for Parallel Synchronized Interworkflows
Shingo Yamaguchi,Tetsushi Narui,Qi-Wei Ge,Minoru Tanaka 대한전자공학회 2008 ITC-CSCC :International Technical Conference on Ci Vol.2008 No.7
An interworkflow N is constructed by connecting a workflow NX with another workflow NY , so interworkflow N should inherit the behavior from workflow NX (and workflow NY). Behavioral inheritance guarantees that interworkflow N can be substituted for workflow NX. Nevertheless it may happen that the behavior is not inherited. Behavioral inheritance can be verified by comparing the reachability graphs of the WF-nets representing interworkflow N and workflow NX. However this verification method is limited to small interworkflows due to the complexity of the state-space explosion. Focusing on a pattern of interworkflows, called Parallel synchronized pattern, we propose a condition to verify behavioral inheritance of Parallel synchronized interworkflows. This condition enables us to verify the behavioral inheritance in polynomial time.
On Verification of Marking-Dependent Terminacy for Data-Flow Program Nets
Shingo Yamaguchi,Keisuke Komiya,Qi-Wei Ge,Minoru Tanaka 대한전자공학회 2008 ITC-CSCC :International Technical Conference on Ci Vol.2008 No.7
In this paper, we discuss terminacy at the initial marking for (data-flow) program nets. Ge et al. have proposed an algorithm to verify terminacy at any marking, i.e. structurally terminacy. However, there is no algorithm to verify terminacy at the initial marking. In this paper, we give a necessary and sufficient condition to verify the terminacy. Using this condition, we construct a polynomial time algorithm for a subclass of program nets. We also show that the problem to verify the terminacy for general program nets is undecidable.
A Soundness Verification Tool Based on the SPIN Model Checker for Acyclic Workflow Nets
Shingo YAMAGUCHI,Munenori YAMAGUCHI,Minoru TANAKA 대한전자공학회 2008 ITC-CSCC :International Technical Conference on Ci Vol.2008 No.7
Workflow nets (WF-nets) are Petri nets for modeling workflows, and are utilized to verification and performance evaluation of workflows. A WF-net should have a property, called soundeness, which guarantees a logical correctness of the modeled workflow. If a given WF-net is free choice then its soundness can be verified in polynomial time. Otherwise there is no polynomial time method to verify soundness for general WF-nets. Unfortunately, some workflows cannot be represented as free choice WF-nets. For example, the WF-net representing an inter-organizational workflow may become asymmetric choice. Thus an efficient method is required. In this paper, we propose a tool to verify soundness using the SPIN model checker. We also show efficiency of our tool by comparing it with an existing WF-nets analysis tool, Woflan, on verification time for asymmetric choice WF-nets.
A Proposal of Refactoring toWell-StructuredWorkflow Nets
Yuki Kuroda,Shingo Yamaguchi,Minoru Tanaka 대한전자공학회 2009 ITC-CSCC :International Technical Conference on Ci Vol.2009 No.7
In this paper, we discuss refactoring free choice workflow nets (WF-net for short) to well-structured ones. It is known that most actual workflows can be modeled as free choice or well-strcutured WF-nets. There are more analysis methods for well-structured WF-nets. Refactoring free choice WF-nets to well-structured ones enables us to apply many analysis methods to free choice ones. We propose two rules for the refactoring. And we show an example of refactroing a WF-net, which represents the actual workflow for an travel agency.