TY - GEN
T1 - Towards a formal verification approach for implementation of web services specifications
AU - Yang, Qing
AU - Ma, Dianfu
AU - Zhao, Yongwang
AU - Li, Zhuqing
PY - 2010
Y1 - 2010
N2 - The implementation of Web services specifications is the key issue of Web services container which is the infrastructure of SOC. The specifications are always depicted in natural language, which may lead to misunderstanding or ambiguity. In this situation, the implementations of the same specification by different containers will re-introduce interoperability which is supposedly addressed byWeb services. These may lead to the reliability problems among upper applications. Currently, formal methods is a precise mathematic way to model the specifications and verify the correctness of the properties. To solve the issues, first, we introduce an XML programming language called SODL (Service-Oriented Description Language) to describe the implementation of specifications. Then, using SODL, we describe the message processing logic according to specifications and implement a Web services container. Furthermore, the logic described in SODL can be converted to automata, by which lots of tools can be applied to verify the properties of container according to the specifications.
AB - The implementation of Web services specifications is the key issue of Web services container which is the infrastructure of SOC. The specifications are always depicted in natural language, which may lead to misunderstanding or ambiguity. In this situation, the implementations of the same specification by different containers will re-introduce interoperability which is supposedly addressed byWeb services. These may lead to the reliability problems among upper applications. Currently, formal methods is a precise mathematic way to model the specifications and verify the correctness of the properties. To solve the issues, first, we introduce an XML programming language called SODL (Service-Oriented Description Language) to describe the implementation of specifications. Then, using SODL, we describe the message processing logic according to specifications and implement a Web services container. Furthermore, the logic described in SODL can be converted to automata, by which lots of tools can be applied to verify the properties of container according to the specifications.
KW - Container
KW - Formal methods
KW - Programming language
KW - Specification
KW - Verification
UR - https://www.scopus.com/pages/publications/79952369419
U2 - 10.1109/APSCC.2010.14
DO - 10.1109/APSCC.2010.14
M3 - 会议稿件
AN - SCOPUS:79952369419
SN - 9780769543055
T3 - Proceedings - 2010 IEEE Asia-Pacific Services Computing Conference, APSCC 2010
SP - 269
EP - 276
BT - Proceedings - 2010 IEEE Asia-Pacific Services Computing Conference, APSCC 2010
T2 - 2010 IEEE Asia-Pacific Services Computing Conference, APSCC 2010
Y2 - 6 December 2010 through 10 December 2010
ER -