Resolving inconsistencies in EFSM-modeled specifications

The US Department of Defense requires that all digital ASIC systems used within the department´s branches should be specified in VHDL (very high speed integrated circuit hardware description language). VHDL specifications are typically modeled as extended finite-state machines (EFSMs). Developing efficient algorithms for EFSM models to generate feasible test sequences with acceptable lengths is a challenging task partly because of the inconsistencies among the actions and the conditions. Inconsistency detection algorithms for EFSM models have been developed at the earlier stages of this study. As part of realizable test sequence generation for VHDL specifications, this paper presents algorithms for the removal of inconsistencies in EFSM models. The proposed method allows the direct application of the FSM-based test generation methods by transforming the EFSM models into equivalent FSMs while avoiding the well-known state explosion problem, where possible. The inconsistency detection and removal algorithms are planned to be applied to the communication protocols used within US Army CECOM and NATO