Favorite Formal Methods
I am a frequent and enthusiastic user of two modeling languages and
their analyzers.
Alloy
Alloy's streamlined combination of predicate logic and relational
algebra makes modeling a pleasure.
I use Alloy and the
Alloy Analyzer
for studies of naming, routing, message paths, and connections in the
Internet (see the Alloy models in
Modeling the Internet from an Application
Perspective).
Promela
Promela is the modeling language of the LTL model checker
Spin.
I use it for all my studies of telecommunication protocols.
There is no real competition because Promela has built-in queues,
which are indispensable for modeling network protocols.