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 Pat... View More