[pgpool-hackers: 3435] Possiblity to apply formal method
ishii at sraoss.co.jp
Wed Sep 18 10:46:19 JST 2019
I accidentally found a formal model system TLA+.
This allows to check a model of concurrent system written in special
language to satisfy certain constrains, such as halting problem and
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+.
SRA OSS, Inc. Japan
More information about the pgpool-hackers