Using the B Method for the Formalization of Coordinated Atomic Actions

摘要

Coordinated Atomic Actions have been proven successful for building dependable distributed systems due to their support for error recovery for both competitive and cooperative concurrent activities. This chapter introduces the formal specification of Coordinated Atomic Actions emphasizing the formalization of proposed dependability mechanisms using the B formal method. The specification then allows developing dependable systems, where the B formal specification can be refined to obtain a correct implementation of the associated runtime support.