s?
Sorry - I get a bit carried away on this topic... For requirements engineering verification one can google: formal and semi-f ormal requirements specification languages. RDAL and ReqSpec are ones I am familiar with. Techniques to verify requirements include model checking. Google model che cking. Based of formal logic like LTL (Linear temporal logic) CTL (Composi tional Tree Logic. One constructs state models from requirements and uses m odel checking engines to analyze the structures. Model checking was actuall y used to verify a bus protocol in the early 90s and found *lots* of proble ms with the spec...that caused industry to 'wake up'. There are others that work on code, but these are very much research-y effo rts.
Simulink has a model checker in its toolboxes (based on Promala) it is quit e good).
We advocate using architecture design languages (ADL's) that is a formal mo deling notation to model different views of the architecture and capture pr operties of the system from which analysis can be done (e.g. signal latency , variable format and property consistency, processor utilization, bandwidt h capacity, hazard analysis, etc.) The one that I had a hand in designing is Architecture Analysis and Design Language (AADL) It is an SAE Aerospace standard. IF things turn out well, it will be used on the next generation o f helecopters for the army. We have been piloting it use on real systems f or the last 2-3 years, and last 10 years on pilot studies. For systems hazard analysis, google STPA (System Theoretic Process Approac h) spearheaded by Nancy Leveson MIT (She has consulted to Boeing).
Yes, I've seen software applied to fix hw problems but assessing the risk i s complicated. The results can be catastrophic. Ok, off my rant....