Petri Net Modeling and Automated Software Safety Analysis: Methodology for an Embedded Military Application

摘要

This thesis investigates the feasibility of software safety analysis using Petri net modeling and an automated suite of Petri Net Utilities (P-NUT) developed at UC Irvine. We briefly introduce software safety concepts, Petri nets, reachability theory, and the use of P-NUT. We then develop a methodology to combine these ideas for efficient and effective preliminary safety analysis of a real-time, embedded software, military system. The system under investigation is a proposed air-to-air guided missile safety and arming device, developed at the Naval Weapons Center in China Lake, California. Although this particular safety arming device was never actually constructed, a software prototype was written and tested. This device is excellent for developing a methodology to analyzed safety-critical computer/software-controlled systems. The device is nontrivial, contains embedded software, and if designed incorrectly or tested ineffectively might result in personal injury or unwanted property destruction. Keywords: Guided missile safety. (AW)