An approach to using Golang programs for the specification and verification of distributed systems

The work is devoted to an attempt to use Golang programs for the specification and verification of distributed systems. The A.P. Ershov Institute of Informatics Systems, SB RAS, has been developing this approach for years. A distributed system described in terms of an SDL specification, which is first translated to a Dynamic-REAL (dREAL) specification, and then to a Promela specification. All these languages (SDL, dREAL, and Promela) are based on the channel concept. Since the Go language (Golang) shares the same feature, we had an idea to use it in some manner. One way is to use Golang to describe distributed systems. However, it is more practical to try to formally verify the already existing Golang applications by translating them into dREAL specifications (as it is done with SDL specifications) or directly into Promela specifications. The paper compares the aforesaid languages and presents a case study of a specification of a simplified ATM network specified in terms of a Golang program.