● 摘要
目前，软件在关键系统中所占的比例越来越高，这就对软件的安全性提出了更高的要求。为了能够有效的提高软件的安全性并节约时间成本，最有效的方式是在软件生命周期的初始阶段——需求阶段就找出软件中可能存在的问题，消除潜在的缺陷。
然而，大部分软件需求都是用自然语言的形式书写的。自然语言形式表示的软件需求易于理解，并能够表达丰富的语义。但对于安全关键系统的软件需求，自然语言描述中出现的歧义性、模糊等问题可能会造成严重的后果。形式化的需求描述方法可以解决自然语言描述中出现的歧义性、模糊等问题，有效的提高软件质，目前得到了越来越多的应用。
但是，通过形式化方法对软件需求进行描述同样存在一些缺陷。首先，建立软件的形式化需求模型缺乏规范有效的方法，一般只是通过专业人员的经验建立需求模型。其次，形式化方法描述的需求难以理解，需要专业的知识才能理解这些形式化的模型。由于这些问题，形式化方法往往只能应用于一些特定的领域，难以推广使用。
为了解决这个问题，本文提出了一种方法。该方法首先将自然语言描述的需求表示一种利用STAMP模型表达的实体——函数模型，再将这种模型表示的需求转化为一种形式化的需求模型——自动机模型。通过这种方法，自然语言表示的需求能够通过一种规范的方式为自动机表示的需求，解决了自然语言中存在的歧义性、模糊等问题，并将形式化模型与自然语言联系起来。除此之外，本文利用AND/OR表描述自动机所表述的需求，使形式化描述的需求更易于理解。本文通过这些技术，解决了形式化方法在实际使用中存在的这两个问题，有利于形式化方法在实际工程中的推广和使用。
在文章的最后，针对一个实际系统，采用本文的研究成果，使用其需求进行了形式化的建模，验证了本文研究成果的有效性。