A software safety analysis method based on S-invariant of Petri Net

With the constant improvement of software complexity, the safety has become an important factor in software development and use. Especially in aviation, safety accidents usually lead to serious personal injuries and economic losses. As a mathematical modeling and analyzing tool, Petri Net can serve as effective means in analyzing system safety during the software development stage. The traditional safety analysis method based on Petri Net requires complete reachable graph and reachable set, so the workload is heavy and state combinatorial explosion may occur when facing complicated system. While the reverse analysis usually cannot guarantee the reachability of hazardous conditions and would result in redundant analysis on the state that is actually unreachable. This thesis proposes the safety analysis method based on S-invariant, which better remedies the defects of the traditional means and greatly reduces the analyzing workload. Lastly, taking certain flight control system software as an example, this thesis carries out safety analysis and compares with the traditional means, thus verifying the usability of the method.