基于控制机制的软件可靠性新技术及其理论研究

近年来软件工程领域发起了对运行时验证的研究，以弥补模型检查技术存在的状态爆炸等弱点。但目前运行时验证在很多方面仍未成熟。第一，运行时验证仅仅监测错误的存在，而不能对系统进行运行时控制，以达到安全保护或错误恢复的目的；第二，运行时验证的基础理论并不成熟，比如可监测性问题等重要理论问题没有得到很好的解决。本项目将把控制机制引入软件工程和软件可靠性领域。这一新机制有以下几个目的：第一，使得规约不仅仅被用于验证，也可以用于对系统进行监测和正确性控制，提供一种新的确保可靠性和安全性的方法；第二，为运行时验证和控制提供理论基础，解决一些重要的理论问题，并在此基础上发展软件验证和控制的新理论和新技术。从理论研究的角度上，我们将提出形式控制系统理论来作为一个统一的理论框架，并探讨该模型及其特例的各种性质。从应用基础研究的角度上，我们将提出并探讨基于控制机制的模型监测方法及其在软件验证和控制中的应用。

本项目属于软件工程领域，主要研究方向是如何将控制机制用于确保软件可靠性，使得正确性需求规约不仅仅被用于验证，还可以用于对系统进行监测和控制。首先，本项目提出了形式化控制系统理论，给出了形式化控制系统的形式化定义，对其理论性质进行研究，证明了各种控制系统的生成能力和表达能力，并建立自动机控制系统和文法控制系统之间的相互转化关系和转化方法，并探讨了基于无限长度单词的控制系统的生成能力。形式化控制系统的科学意义在于提供了一种更加通用的控制理论框架。第二，本项目研究了基于形式化控制系统理论的运行时监测、验证和控制方法，这些方法和技术可以对程序进行运行时验证和控制，从而提高软件系统的可靠性和安全性。项目组实现了一个使用这些技术的原型系统，可以对C语言程序构造基于控制机制的验证器，实验证明了这些技术的可行性，可以为正确性需求规约的变化和演化提供更好的支持。最后，本项目也研究了软件验证技术的实际应用，实验证明形式化验证可以有效地用于实际机载软件、网络路由协议和Web服务等系统的验证问题。