The method of formalizing computational algorithms using the hierarchical Petri nets is considered. Software package which implements this method is developed. This software package allows you to analyze models of software algorithms for deadlocks, impracticable operations, loops and infinite looping. A method is based on one of the analysis methods of Petri nets - reachability tree.