Paper Info
Title
The Validation and Verification of WSCDL
Abstract
This paper presents an approach to validation and verification of the WSCDL specification. In order to validate whether the CDL document is well defined or not, we introduce OCL to precisely describe the constraints which was expressed by natural language, and design a simple validator to check the static properties of the CDL document. The validator is created based on a Java model and the Java model is generated according to the UML diagrams with OCL constraints which is used to describe CDL specification. To verify the dynamic properties of CDL document, we model the behavior of CDL document with Java, so that Java Pathfinder model checker can be applied to check the desired properties. The assert activity is introduced to the CDL specification for describing the logic properties, to facilitate the verification process. A case study is given and it shows that our approach is both effective and practical. Moreover, this approach can check almost every kinds of CDL document, even the documents including exception block or finalize block.
Year
DOI
Venue
2007
10.1109/APSEC.2007.93
APSEC
Keywords
Field
DocType
simple validator,exception block,wscdl specification,cdl specification,cdl document,java pathfinder model checker,verification process,ocl constraint,java model,finalize block,formal verification,formal specification,verification,unified modeling language,validation and verification,web services,java,natural language
Programming language,Model checking,Unified Modeling Language,Verification and validation,Computer science,Formal specification,Natural language,Java,Formal verification,Validator
Conference
ISBN
Citations 
PageRank 
0-7695-3057-5
5
0.53
References 
Authors
11
6
Name
Order
Citations
PageRank
Geguang Pu160257.89
Jianqi Shi25712.50
Zheng Wang343192.42
Lu Jin450.53
Jing Liu530234.34
He Jifeng61771190.43