Abstract: With Extended Finite State Machine（EFSM） being applied widely in the fields of computer science and engineering，the design of EFSM is becoming an important issue.However，existing design methods for EFSM lack rigorous theoretical foundation and therefore have to rely heavily on the experience of personal.In this paper，the supervisory control theory of discrete event systems are suggested to be a theoretical foundation to EFSM design，since a transition predicate of an EFSM can be seen as a supervisor of the transition.Firstly，the EFSM induced by a Finite State Machine（FSM） and its language are introduced.Then，based on a plant and its supervisor in the supervisory control theory of discrete event systems，an approach to design EFSM is presented and a rigorous foundation to EFSM design is provided.At the end，this paper illustrates the approach by a password protection module and a software testing process.

Key words: formal method, software cybernetics, discrete event dynamic system, Extended Finite State Machines（EFSM）, Finite State Machines（FSM）

摘要： 随着扩展有限状态机（EFSM）模型在计算机科学和工程领域的广泛应用，EFSM的设计逐渐成为一个重要的问题。目前EFSM的设计仍然主要依赖于个人经验，缺乏理论基础。由于EFSM中每个转移的谓词可以看作此转移的一个监控器，所以可以用离散事件系统的监控理论为EFSM设计提供理论基础。首先定义了有限状态机（FSM）导出的EFSM及其产生的语言。然后，基于监控理论中的受控对象和监控器，提出了一种设计EFSM的方法，用离散事件系统监控理论为EFSM设计提供理论依据。最后用两个实际例子说明了提出方法的可用性和有用性。

关键词: 形式化方法, 软件控制论, 离散事件系统, 扩展有限状态机（EFSM）, 有限状态机（FSM）