July 7, 2008 to July 11, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SCC.2008.67
Abstract Recovery is the last resort when other components exhibit bugs. It is therefore of paramount importance that the correctness of the recovery protocols be formally verified. Recovery not only needs to cope with database failures but should handle and ideally mask message and process failures in clients and servers. Otherwise, when a reply message is lost the application must be able to determine "manually" whether the interaction is to be repeated. This paper develops a statechart specification of a recovery framework that generically guarantees exactly-once execution and applies model checking to prove its correctness.
recovery, formal methods, statechart, model checking
German Shegalov, Gerhard Weikum, "Formal Verification of Web Service Interaction Contracts", SCC, 2008, 2013 IEEE International Conference on Services Computing, 2013 IEEE International Conference on Services Computing 2008, pp. 525-528, doi:10.1109/SCC.2008.67