[pgpool-hackers: 3435] Possiblity to apply formal method

[Tatsuo Ishii]

I accidentally found a formal model system TLA+.

https://lamport.azurewebsites.net/tla/toolbox.html
https://en.wikipedia.org/wiki/TLA%2B

This allows to check a model of concurrent system written in special
language to satisfy certain constrains, such as halting problem　and
reachability problem.

Since watchdog is a state machine, I guess it is possible to write a
model of it. Once we succeed in creating a model, we could verify the
correctness of the model by using tools provided by TLA+.

Best regards,
--
Tatsuo Ishii
SRA OSS, Inc. Japan
English: http://www.sraoss.co.jp/index_en.php
Japanese:http://www.sraoss.co.jp