Digital computers have been chosen in the implementation of safety critical systems in newly constructed nuclear facilities. These safety critical systems are designed to operate in a secure manner so that their failure should not prompt any serious damage or catastrophic effects. Due to the security significance of critical systems, there is a need to ensure the secrecy of systems at an early stage. Existing work focused on evaluating security by considering at the requirement phase only integrity, confidentiality, access control, and availability attributes. However, many essential critical attributes have not been taken into consideration, like deadlock, liveness, etc. To improve the security of software systems, this paper introduces a threat-driven modeling framework. It predicts security threats, it figures out which threats require mitigation and how to alleviate these threats, and it incorporates the essential missing attributes. We specify the functionality of the system with a Petri net, and we analyze the behavioral and structural properties of the system and threat mitigation. Aspect-oriented stochastic Petri nets are used as a formal amplified model. The technique has been validated on 11 safety critical systems of a nuclear power plant and it is shown for one case study in this paper.