Formalizing and Verification of an Antivirus Protection Service using Model Checking
Adalat Safarkhanlou, Alireza Souri, Monire Norouzi, SeyedHassan Es. Haghi Sardroud · Procedia Computer Science · 2015
In this paper, a protection service model is proposed for an antivirus system. The proposed model has been focused on maintaining in secure state of the system. According to the proposed antivirus model, the required behavior has been specified as extended state machine diagrams and translated to temporal logic properties by using Computing Tree Logic language. Also the proposed model has been converted to aKripke Structure by using formal verification techniques. For proving the correctness and the reachability of proposed model, some properties of the proposed model are verified by using NuSMV model checker.