Alireza Souri, Solmaz Abdollahizad, Majid Samad Zamini and Adalat Safarkhanlou
Keywords: Real-time security protection service, dynamic link library, model checking, NuSMV
Abstract: In this paper a real-time security protection model for scanning the security files is presented. In this model, a workflow mechanism is presented for real-time scanning Dynamic Link Library files. A specification relation between the proposed model and the Kripke structure is presented that enables the verification of the system specifications. By presenting the appropriate formal semantics, we discuss that how labeling functions permits navigating information and specifications of the security system. We illustrated expected properties of the system which can be verified and specified by using temporal logic. So, we defined satisfaction relations for verifying the system specifications. We also described how some of expected properties of the system are verified. Finally, we implemented some properties of proposed model in NuSMV model checker. The verification results show that our proposed real-time security protection model is reachable, deadlock free and fair
[View Complete Article]