[nickpsecurity]

They're good evrn for exploration if you're using formal specs. Reason is good ones knock out errors due to English ambiguity and inconsistencies. Z, Navy's SCR, B method, and Statecharts were all used for these purposes with success. Executable specifications did even better for exploration aspect.

Current research is taking it further with code generation from specs like AADL, UML, and especially SCADE/Esterel.