Journals Proceedings

Abstract

This paper studies the safety issues of the synchronous composition of Finite State Machines (FSMs). Synchronous FSM composition is widely used when designing and analyzing various aspects in hardware implementation including so-called Trojan subcircuits. When an external input sequence is applied and component FSMs cannot agree on matched internal actions or there are different matching options, the sequence can destruct or block a corresponding device and thus, should be clearly avoided. In this paper, we propose a formal approach for analyzing which external input sequence can induce such situations (if any) and then to derive a finite automaton that represents the set of all possible safe external input sequences.