Logic-based Modeling, Analysis, and Implementation of Workflow
Management Systems
IIS-0072927
Principal Investigator
Michael
Kifer
Department of Computer Science
Stony Brook University
Department of Computer Science
Stony Brook University,
Stony Brook,
NY
11794-4400
631-632-8459
631-632-8334
kifer@cs.stonybrook.edu
http://www.cs.sunysb.edu/~kifer
Co-PI
C.R.
Ramakrishnan
Department of Computer Science
Stony Brook University
Department of Computer Science
Stony Brook University,
Stony Brook,
NY
11794-4400
631-632-8334
cram@cs.stonybrook.edu
http://www.cs.sunysb.edu/~cram
Co-PI
I.V.
Ramakrishnan
Department of Computer Science
Stony Brook University
Department of Computer Science
Stony Brook University,
Stony Brook,
NY
11794-4400
631-632-8334
ram@cs.stonybrook.edu
http://www.cs.sunysb.edu/~ram
Keywords
workflow,
verification,
logical analysis ,
web services,
semantic web
Project Summary
A workflow is a collection of
coordinated activities designed to carry out a well-defined
complex process, such as trip planning
or a business process in a large
enterprise. An activity in a workflow might be performed by a
human, a device, or a program. Workflow management systems
(WfMS) provide a framework for capturing the interaction among
the activities in a workflow and are recognized as a new
paradigm for integrating disparate systems, including legacy
systems. Automated workflow management is becoming increasingly
important, as it is one of the enabling technologies for
business-to-business e-commerce. Ideally, a WfMS should be able
to help the user in analyzing and reasoning about complex
business processes. Unfortunately, present-day systems do not
provide sufficient support for this activity and the virtual
lack of analysis and reasoning facilities in current workflow
management systems is considered a serious problem. To tackle
this problem, a formal specification model with a well defined
semantics is needed. The objective of the proposed project is
to conduct research in workflow management and to develop both
the scientific and technological infrastructure for
implementing verifiable workflow management systems.
Publications and Products
- Publications
-
A Logical Framework for Scheduling Workflows Under
Resource Allocation
Constraints (P. Senkul, M. Kifer,
I.H. Toroslu). VLDB 2002.
-
Well-Founded Optimism: Inheritance in
Object-Oriented Knowledge Bases
(G. Yang and M. Kifer). ODBASE 2002.
-
On the Semantics of Anonymous
Identity and Reification (G. Yang and
M. Kifer). ODBASE 2002.
-
Extraction Techniques for Mining Services from Web
Sources (Hasan Davulcu, Saikat Mukherjee, IV
Ramakrishnan). IEEE International Conference on
Data Mining (ICDM), 2002.
-
Efficient Model Checking of Real Time Systems Using
Tabled Logic Programming and Constraints
(G. Pemmasani, C. R. Ramakrishnan,
I. V. Ramakrishnan).
International Conference on Logic Programming
(ICLP), Lecture Notes in Computer Science, pages
100--114, Springer, 2002.
-
Compositional Analysis for Verification of
Parameterized Systems (S. Basu,
C. R. Ramakrishnan). Ninth International
Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS),
Lecture Notes in Computer Science, pages 315--330,
Springer, 2003.
-
Inheritance and Rules in
Object-Oriented Semantic Web Languages
(G. Yang and M. Kifer).
Rules and Rule Markup Languages for the Semantic
Web (RuleML03),
Springer Verlag, 2003.
-
Annotating Content-Rich Web Documents: Structural
and Semantic Analysis (Saikat Mukherjee, Guizhen
Yang, IV Ramakrishnan). International Semantic Web
Conference (ISWC), 2003
-
Automatic Discovery of Semantic Structures in HTML
Documents (Saikat Mukherjee, Guizhen Yang, Wenfang
Tan, IV Ramakrishnan). International Conference on
Document Analysis and Recognition (ICDAR), 2003
-
On the Power of Semantic Partitioning of Web
Documents (Guizhen Yang, Saikat Mukherjee, Wenfang
Tan, IV Ramakrishnan, Hasan Davulcu) IJCAI
Workshop of Information Integration on the Web
(WIIW), 2003.
-
On the Complexity of Schema Inference from Web
Pages in the Presence of Nullable Data Attributes
(G. Yang, I. V. Ramakrishnan, M. Kifer).
Conference on Information and Knowledge Management
(CIKM). 2003.
-
Reasoning about Anonymous
Resources and Meta Statements on the Semantic Web
(G. Yang and M. Kifer). Journal
of Data Semantics, 2004.
-
Logic Based Approaches to Workflow Modeling and
Verification (H. Davulcu, M. Kifer, S. Mukherjee,
P. Senkul, G. Yang). In Logics for Emerging
Applications of Databases, eds. J. Chomicki, R. van
der Meyden and G. Saake, Springer-Verlag, 2003.
- Other products:
Flora-2:
This is an object-oriented knowledge-base
programming system based on F-logic, HiLog, and
Transaction Logic.
XMC
is a model checker implemented using the XSB
tabled logic programming system. It is an
explicit-state, local model checker for processes
specified in XL, a version of value-passing
CCS, and the alternation-free fragment of the modal
mu-calculus.
Project Impact
The project has produced results in several areas:
workflow systems, Semantic Web, and verification of
concurrent systems. It has been supporting, in part, six
Ph.D. students, one research associate, and one post-doc.
Some results from this project have helped a startup, XSB
Inc., to receive Phase I and II SBIR funding from NSF for
their WEAVE project.
The project supported the development of two systems:
Flora-2 and XMC, which have dozens of users.
Goals, Objectives and Targeted Activities
- Workflow modeling and scheduling
-
We have developed a new language, called CTR-S, for
reasoning about workflow environments where tasks don't
cooperate or their behavior is not fully specified.
CTR-S was found to be appropriate
for describing Web service contracts -- an emerging
subfield of Semantic Web Services.
-
We have developed techniques for specifying and
scheduling workflows in the presence of control and
aggregate cost constraints.
- Verification of workflows
-
Verification of unbounded
number of concurrent workflow instances
is based on compositional model checking
and program analysis for automatic verification of
infinite families of systems.
-
Verification of workflows with real-time constraints is
based on a technique that uses difference bound matrices
(DBMs). An implementation based on this technique is
considerably faster than our earlier prototype and shows
very good memory use.
- Semantic Web mining
We developed two kinds of technologies, one based on a
supervised approach while the other is unsupervised. In
the supervised approach, users create and launch Web
agents from a browser, by creating a 'navigation map' of
the site through the paradigm of 'mapping by example.' In
the unsupervised approach, data extraction is done through
ontology-driven machine learning techniques.
Area Background
A workflow is a collection of coordinated
activities designed to carry out a well-defined process that
can range from something relatively simple like trip planning
to complex manufacturing tasks like supply chain
management. Workflow management systems (abbr., WfMS) provide
a framework for capturing the interaction among the
activities in a workflow and are recognized as a new paradigm
for integrating disparate systems, including legacy systems.
The need for the formal treatment of WfMS arises when
workflows are executed under various constraints, when they
change dynamically, or when the different activities do not
cooperate (as in Web services).
The essence of our approach is in the use a high-level
specification language, Transaction F-logic, which provides
both the reasoning tools as well as a language for executable
specifications.
Area References
Workflow management:
http://www6.informatik.uni-erlangen.de/research/wf_references.html.
Transaction F-logic:
http://flora.sourceforge.net/.
Semantic Web resources:
http://www.SemanticWeb.org
Project Websites
FLORA-2
The site dedicated to the FLORA-2
system. Also has a wealth of related
information about this project.
The Logic-Based Model Checking Project.
Dedicated to the
verification part of
the project.
XMC software can be downloaded here as well.