Specification, composition, and automated verification of layered communication protocols

摘要: Horus is a general-purpose layered message-passing system for distributed programming. A programmer of application can select protocol layers from among those provided by and arrange these in stack, thereby creating custom-built with strong (or not so strong) properties underneath the application. For full value Horus's modularity to be exploited, an must able choose just stacking order that will provide desired properties. who limited only few "tried-and-true" alternatives may end up paying performance cost (such as excessive synchronization messages) unnecessary properties, simply because he or she cannot confidently build less costly stack given application. This dissertation describes formal method supports engineering new stacks precisely specifying mechanically verifying communication stacks. Various described English, but are also succinctly mathematical model (the Temporal Logic Actions) sound reasoning about whether satisfied implementation. Each layer guarantees various at its interfaces, depending on what assumed neighbors it. Relatively straightforward then show certain applications top stack. This efficiently automated it used practitioners. prototype verifier has been implemented Java published World Wide Web.