Verification of the Protection Services in Antivirus Systems by Using Nusmv Model Checker
Monire Norouzi, Saeed Parsa · International Journal in Foundations of Computer Science & Technology · 2014
In this paper, a model of protection services in the antivirus system is proposed. The antivirus system behavior separate in to preventive and control behaviors. We extract the properties which are expected from the model of antivirus system approach from control behavior in the form of CTL and LTL temporal logic formulas. To implement the behavior models of antivirus system approach, the ArgoUML tool and the NuSMV model checker are employed. The results show that the antivirus system approach can detects fairness, reachability, deadlock free and verify some properties of the proposed model verified by using NuSMV model checker.