Using Time Reachability Tree Logic to Specifying and Verifying Temporal Behavior of Workflow-Net

2014 ◽  
Vol 571-572 ◽  
pp. 528-534
Author(s):  
Chyun Chyi Chen ◽  
Yueh Min Huang
Keyword(s):  
Petri Nets ◽  
Workflow Management ◽  
Schedulability Analysis ◽  
Temporal Behavior ◽  
Time Petri Nets ◽  
Reachability Graph ◽  
Workflow Execution ◽  
Workflow System ◽  
Timing Properties ◽  
Reachability Tree

Workflow management has been a hot issue in both academic and industrial research. Deadline assignment is of great significance in workflow management. In order to avoid deadline violation, this paper presents an approach to the schedulability analysis of workflow system modeled in p-time Petri nets by separating timing properties from other behavior properties. The analysis of behavioral properties is conducted based on the reachability graph of the underlying p-Time Petri net, whereas timing constraints are checked in term of absolute and relative firing domains. Our technique is based on a concept called clock-stamped state class (CS-class) and temporal logic. With the reachability graph generated based on CS-class, we can directly compute the end-to-end time delay in workflow execution. We have identified a class of well-structured p-time Petri nets such that their reachability can be easy analyzed and temporal behavior can be easy analyzed by time reachability tree logical.

scholarly journals Embedding Analytics within the Curation of Scientific Workflows

2020 ◽  
Vol 15 (1) ◽  
pp. 8
Author(s):  
Gerard Weatherby ◽  
Michael Robert Gryk
Keyword(s):  
Hybrid Approach ◽  
Workflow Management ◽  
Scientific Data ◽  
Data Reuse ◽  
Biomolecular Nmr ◽  
Domain Experts ◽  
Workflow Execution ◽  
Manual Intervention ◽  
Workflow System ◽  
Computational Workflow

This paper reports on the ongoing activities and curation practices of the National Center for Biomolecular NMR Data Processing and Analysis1. Over the past several years, the Center has been developing and extending computational workflow management software for use by a community of biomolecular NMR spectroscopists. Previous work had been to refactor the workflow system to utilize the PREMIS framework for reporting retrospective provenance as well as for sharing workflows between scientists and to support data reuse. In this paper, we report on our recent efforts to embed analytics within the workflow execution and within provenance tracking. Important metrics for each of the intermediate datasets are included within the corresponding PREMIS intellectual object, which allows for both inspection of the operation of individual actors as well as visualization of the changes throughout a full processing workflow. These metrics can be viewed within the workflow management system or through standalone metadata widgets. Our approach is to support a hybrid approach of both automated, workflow execution as well as manual intervention and metadata management. In this combination, the workflow system and metadata widgets encourage the domain experts to be avid curators of the data which they create, fostering both computational reproducibility and scientific data reuse.  

Schedulability Analysis Algorithm of Timing Constraint Petri Nets

2012 ◽  
Vol 532-533 ◽  
pp. 1810-1814 ◽  
Author(s):  
Hui Fang Li ◽  
Fu Jian Feng
Keyword(s):  
Petri Nets ◽  
Workflow Management ◽  
Schedulability Analysis ◽  
Timing Constraints ◽  
Reliability Engineering ◽  
Timing Constraint ◽  
Constraint Analysis ◽  
Novel Approach ◽  
Two Phases ◽  
Task Sequences

A novel approach to the schedulability analysis is presented in this paper for timing constraint Petri nets, which have wide applications in the workflow management, software engineering, reliability engineering, and so on. The analysis can be conducted in two phases: finding firing sequences and timing constraint analysis, among which the first one is to find the transition sequences that transform the initial marking to a certain marking by using incidence matrix in the underlying Petri net, and the second one is to verify whether the reachable marking found in the first step is reachable with the timing constraints. The proposed method is able to pinpoint out non-schedulable transitions and adjust the timing constraints to make all the transitions schedulable within complex task sequences, while meeting the needs of the managers to schedule the tasks.

SPECIFYING AND VERIFYING TEMPORAL BEHAVIOR OF HIGH ASSURANCE SYSTEMS USING REACHABILITY TREE LOGIC

1999 ◽  
Vol 09 (02) ◽  
pp. 233-249
Author(s):  
STEPHEN J. H. YANG ◽  
WILLIAM CHU ◽  
JONATHAN LEE
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Petri Net ◽  
System Modeling ◽  
Model System ◽  
Temporal Behavior ◽  
Time Petri Net ◽  
High Assurance ◽  
System Requirements ◽  
Reachability Tree

This paper presents our reachability tree logic (RTL) and its integration with time Petri nets to specify and verify the temporal behavior of high assurance systems. The specification phase begins with a system modeling to model system requirements into a time Petri net N and construct a reachability tree RT of N. We then use RTL to specify the desired temporal behavior as formula F. The verification phase uses a model-checking algorithm to check whether RT can satisfy F, that is to find firing sequences to satisfy F. If F is not satisfied, we then modify N into N′ and obtain a RT′ of the modified N′. The modification (refinement) continues until the modified RT′ can satisfy F. In addition, we will demonstrate how to reduce the complexity of model-checking by using our RTL-based algorithm. We have implemented a specification and verification toolkit called NCUPN (National Central University Petri Nets toolkit) using Java. NCUPN is now available on the Internet via

Sign in / Sign up

Export Citation Format

Share Document