Formal Verification of Distributed Master-Slave Finite State Machine
Marko Popović, Vladimir Marinković, Miodrag M. Djukic, Miroslav V. Popovic · 2021 29th Telecommunications Forum (TELFOR) · 2021
Recently, the distributed master-slave finite state machine appeared as a solution to govern a pair of transaction coordinators operating in the master-slave mode. In this paper, we formally verify the correctness of that solution using process algebra CSP and the model checker PAT. The CSP model consists of CSP processes modelling the transaction coordinators and individual master-slave finite state machines. During verification, altogether 30 assertions were automatically checked by PAT and found to be valid.