Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{963627, author = {Ravn, Anders P. and Srba, Jiří and Vighio, Saleem}, address = {Neuveden}, booktitle = {Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'11)}, doi = {http://dx.doi.org/10.1007/978-3-642-19835-9_32}, keywords = {verification; modelling; web services; business activity}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Neuveden}, isbn = {978-3-642-19834-2}, pages = {357-371}, publisher = {Springer-Verlag}, title = {Modelling and Verification of Web Services Business Activity Protocol}, url = {http://www.springerlink.com/content/978-3-642-19834-2}, year = {2011} }
TY - JOUR ID - 963627 AU - Ravn, Anders P. - Srba, Jiří - Vighio, Saleem PY - 2011 TI - Modelling and Verification of Web Services Business Activity Protocol PB - Springer-Verlag CY - Neuveden SN - 9783642198342 KW - verification KW - modelling KW - web services KW - business activity UR - http://www.springerlink.com/content/978-3-642-19834-2 N2 - WS-Business Activity specification defines two coordination protocols in order to ensure a consistent agreement on the outcome of long-running distributed applications. We use the model checker Uppaal to analyse the Business Agreement with Coordination Completion protocol type. Our analyses show that the protocol, as described in the standard specification, violates correct operation by reaching invalid states for all underlying communication media except for the perfect FIFO. Based on this result, we propose changes to the protocol. A further investigation of the modified protocol suggests that messages should be received in the same order as they are sent so that a correct protocol behaviour is preserved. Another important property of communication protocols is that all parties always reach their final states. Based on the verification with different communication models, we prove that our enhanced protocol satisfies this property for asynchronous, unreliable, order-preserving communication whereas the original protocol does not. ER -
RAVN, Anders P., Jiří SRBA a Saleem VIGHIO. Modelling and Verification of Web Services Business Activity Protocol. In \textit{Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ($\{$TACAS$\}$'11)}. Neuveden: Springer-Verlag, 2011, s.~357-371. ISBN~978-3-642-19834-2. Dostupné z: https://dx.doi.org/10.1007/978-3-642-19835-9\_{}32.
|