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

Tatsuo Ishii 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
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

More information about the pgpool-hackers mailing list