Using Propositional Logic for Requirements Verification of Service Workflow

被引:101
作者
Xu, Li Da [1 ,2 ]
Viriyasitavat, Wattana [3 ]
Ruchikachorn, Puripan [3 ]
Martin, Andrew [4 ]
机构
[1] Chinese Acad Sci, Inst Comp Technol, Beijing 100080, Peoples R China
[2] Old Dominion Univ, Dept Informat Technol & Decis Sci, Norfolk, VA 23529 USA
[3] Chulalongkorn Univ, Dept Stat, Fac Commerce & Accountancy, Bangkok 10330, Thailand
[4] Univ Oxford, Dept Comp Sci, Oxford OX1 3QD, Oxon, England
关键词
Compliance checking; enterprise systems; propositional logic; service; service industry; service industry informatics; specification language; workflow; COMPLIANCE CHECKING; TEMPORAL LOGIC; SYSTEMS;
D O I
10.1109/TII.2012.2187908
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
This paper presents a requirement-oriented automated framework for formal verification of service workflows. It is based on our previous work describing the requirement-oriented service workflow specification language called SWSpec. This language has been developed to facilitate workflow composer as well as arbitrary services willing to participate in a workflow to formally and uniformly impose their own requirements. As such, SWSpec provides a formal way to regulate and control workflows. The key component of the to-be-proposed framework centers on verification algorithms that rely on propositional logic. We demonstrate that logic-based workflow verification can be applied to SWSpec which is capable of checking compliance and also detecting conflicts of the imposed requirements. By automating compliance checking process, this framework will support scalable services interoperation in the form of workflows in opened environments.
引用
收藏
页码:639 / 646
页数:8
相关论文
共 25 条
[1]  
Awad A, 2008, LECT NOTES COMPUT SC, V5240, P326, DOI 10.1007/978-3-540-85758-7_24
[2]  
Bi H. H., 2004, J INFORM TECHNOL MAN, V5, P293
[3]  
BLAZE M, 1998, SEC PROT INT WORKSH
[4]   Service-Oriented Infrastructure to Support the Deployment of Evolvable Production Systems [J].
Candido, Goncalo ;
Colombo, Armando W. ;
Barata, Jose ;
Jammes, Francois .
IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 2011, 7 (04) :759-767
[5]  
Cimatti A., 1998, SOFTWARE TOOLS TECHN, V2, P410
[6]  
Clarke E. M., 2000, HDB AUTOMATED REASON
[7]  
Clarke EdmundM., 1981, LECT NOTES COMPUTER, V131
[8]   AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].
CLARKE, EM ;
EMERSON, EA ;
SISTLA, AP .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263
[9]   A Real-Time Service-Oriented Architecture for Industrial Automation [J].
Cucinotta, Tommaso ;
Mancina, Antonio ;
Anastasi, Gaetano F. ;
Lipari, Giuseppe ;
Mangeruca, Leonardo ;
Checcozzo, Roberto ;
Rusina, Fulvio .
IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 2009, 5 (03) :267-277
[10]   USING BRANCHING TIME TEMPORAL LOGIC TO SYNTHESIZE SYNCHRONIZATION SKELETONS [J].
EMERSON, EA ;
CLARKE, EM .
SCIENCE OF COMPUTER PROGRAMMING, 1982, 2 (03) :241-266