Analytic Design Laboratories (ADL) proposes power tools for software Nuclear Safety Cross-Check Analysis (NSCCA). NSCCA exists because there is a vital concern that a nuclear weapon system not do certain things. For example, a nuclear armed missile shall not launch without proper authorization codes, which is a negative requirement. Under other circumstances, the positive requirement would be tested, verifying that the missile launches after accepting authorization codes. But that is not acceptable for a nuclear weapon system. It is necessary to verify that there is in fact no way to launch the missile without authorization codes. Conventionally, negative requirements like this are said to be untestable. NSCCA needs power tools because it is so difficult to verify negative requirements. The ADL NSCCA Power Tools will stabilize the cost of NSCCA while making the NSCCA analyst more effective.
Benefit: ADL"s NSCCA Power Tools will address the daunting task of showing compliance with negative Nuclear Safety Objectives (NSOs). Because NSCCA is difficult and specialized, it is expensive. At one time, NSCCA was expected to be an end-to-end consideration of the entire software program. In these days of budget austerity, the scope is limited to the changes being made to the code and the impacts of those changes on pre-existing code. It is hard to know when to quit analyzing existing code. There are examples of issues missed because impacts on pre-existing code were not fully contemplated. The ADL NSCCA Power Tools will automatically trace all of the requirements into the code and ensure that testing is end-to-end. By automating many of the mundane tasks, the NSCCA personnel will spend more of their time understanding the nuclear critical software.
Keywords: NSCCA, IV&V, formal
