"The reason this stopped, people retired."

Sorry to hear that. I'm short on suggestions for that one given I focus on getting tools adopted more than re-adopted. I'll have to look into that scenario a bit given I bet it plays out a lot.

"I've read a number of your posts, usually when I see your handle I make a point to read them regardless of how long they are. And sometimes I realize it's you just by the content and look for more in a thread. In principle I think we're on the same page"

Appreciate the kind words. I work hard to get the quality stuff out there to people like you. Hard to assess how it's being received. Comments like that and occasional emails are what I go on for impact assessment.

"A test case may involve dozens or hundreds of key messages to simulate a "conversation" between two or more radios to determine how our software behaves, with thousands more sent automatically. "

Ohhhh. Ok. I'm already seeing it based on prior experience testing both protocols and UI's. Yeah, that would take a lot of testing if specs were out of date or insufficient. With specs, you could use design-by-contract on it to support testing with interface checks and/or auto-generate tests depending on tooling. I mean, the Fortran static analysis tooling might be behind a bit... (read: nonexistent).

"but never finished, going through all the messages that could be sent and what the responses ought to be and when to try to produce a better simulator than we presently use"

Are you actually able to change the protocol in arbitrary ways so long as product functions properly in some other black box your company can control? Or do you have to maintain its existing, functional behavior for backward compatibility? If the former, you can gradually spec it out then maybe apply a protocol generator. If the latter, it might stay pretty manual with DbC, testing, and/or static analysis being best you're going to do.

"In a past life I worked with LDRA "

Oh, you got to work with one of the real ones. Good for you. I haven't been able to afford them so I keep trying to get comments on how effective or usable they are. Did it catch stuff well? Make it fairly easy to do requirements/spec/code consistency or lots of redundancy for user? On the latter, point is that high-assurance development requires a number of documents that all describe the same thing. Essentially views on the operation of the system. How easily a tool can keep them together and/or propagate changes in one to another is important to avoid people saying "screw it: i'll update that later [never]." So, I'm curious about its usability. Still no consensus on tools for that with Topcased being an open one some went with, some using traditional SCM w/ specs/docs in it, some HTML (eg LISP spec), and Karger et al on Caernarvon used Framemaker with lots of cross-links.

"we used Telelogic DOORS"

Could've been interesting but IBM acquired it for Rational suite. Nevermind.

"wanted to use SPARK Ada but found the documentation at the time to be sparse online"

Might be worth re-exploring given they've done a lot over the years. SPARK 2014 was quite an update. Almost nobody does anything with it but there is a DNS server written in it. Might contain insight on applying SPARK to protocol design/verification. Not to mention its other, potential benefits. :)

http://ironsides.martincarlisle.com/