从上世纪五十年代软件诞生开始，软件设计一直是软件系统开发的核心内容，好的软件设计有助于软件开发人员提高工作效率，减少不必要的开支以及保证软件的正确性。但采用何种方法来保证软件设计是“好的”　　 一直是软件开发人员关注的问题。从最初靠个人智慧来设计和编写软件，到各种软件设计方法“百家争鸣”，再到众所周知的统一建模语言，研究者们一直试图找到一种理想的设计方法一这种设计方法易于被使用者理解和接受，便于使用和交流，规范且能保证设计的正确性，这种语言至今并未出现，目前的设计语言只能满足上述部分方面。到了上世纪末，出现了两种风格迥异的设计方法，一种方法提倡简单灵活，既不使用复杂的数学理论作为基础，也不使用严谨的设计方式保证正确性，这种方法就是已经被大多数设计人员和团队接受的统一建模语言；另一种方法认为在软件设计阶段用精确和严谨的证明保证系统的正确性是必不可少的，提倡采用规范可证明方式来设计软件。但由于需要使用者具有较好的数学基础，普及成本较高，加上技术并不成熟以及没有好的工具支持，使得这种方法目前仍处于试验阶段，并未普及，如VDM方法、B方法、Z方法等。　　 本文提出了一种使用CHAM化学抽象机形式化语言对状态图进行形式化的方法，之所以选择化学抽象机形式化语言，因为这种语言最初用于并行计算的描述，具有严谨的数学基础和完整的语义，之后，用于系统行为的描述，具有一定的动态描述能力，有可能实现状态图的形式化，本文采用一种新的状态图的划分方法，将状态图分为简单状态图，分层状态图和并发状态图三种，并分别论述了形式化描述的方法，并用一个概括性的实例展示了具体实现方式。　　 在上述研究基础上，本文提出一种可用于化学抽象机形式化语言书写的工具，该工具有效的支持化学抽象机形式化语言描述，采用了规则检验等方式保证正确性，并引用自动生成溶液的方式以减少书写的工作量，解决了之前CHAM语言没有工具支持的问题。