从形式化式样出发的实时控制软件开发

形式化语言能够对软件的功能进行精确的描述,在实时控制软件中引入形式化语言描述是必要的也是可能的。本文介绍了形式化式样语言VDM-SL(ViennaDevelopmentMethod-SpecificationLanguage),用VDM-SL给出了一个小型控制软件的形式化描述。基于形式化式样描述,提出了从形式化式样出发的控制软件开发。最后就形式化语言应用于软件描述的前景进行了分析,同时指出了形式化语言和工具的不足。

This paper introduces VDM-SL and gives a Formal description of a small-scale control software using VDM-SL.Then control software programming from formal specification is proposed.Finally the prospect and the incapability of Formal Method is covered.