Checking software security using EFSMs

The paper is devoted to analyzing unsafe features of an Extended Finite State Machine such as the exceeding of the value of a context variable and/or an output parameter, the reachability of critical states, etc. As the ordinary simulation of an EFSM is very complex, the well known verifier Java Path Finder is used for this purpose. The EFSM is implemented as a template Java code that is checked for critical situations by the above verifier. The efficiency of a proposed approach is illustrated by an example.