A lot of folks liked Just Enough Structured Analysis by Yourdon. Yourdon's methods date back to the 1970's with a lot of real-world application. That approach was also used in at least one high-assurance system (Tenix Data Diode).

http://zimmer.csufresno.edu/~sasanr/Teaching-Material/SAD/JE...