A Fundamental Research for Formal Models and Verification Techniques of Open Software

我们已经研究了“开放软件”的适当的正式框架，它在与环境的通信中表现出反应性。在通信过程模型的基础上，重点研究了开放软件的形式化语义的建立和验证技术。我们取得的成果如下：(1)提出了通信进程模型的时间扩展，并导出了有效的验证替换特征；(2)提出了通信进程模型的概率扩展，导出了有效的替换验证特征；(3)提出了具有时间一致性和良好定义的结构化操作语义规范的通用框架；(4)利用多自认知逻辑研究了开放软件的逻辑描述；(5)基于诊断信息生成，构建了一个用于有效调试的原型编程环境(6)提出了一种中间描述，它既可以抽象为LOTOS规格说明，又可以扩展为C程序。

We have investigated the appropriate formal framework for "open software" that behaves reactively on communications with the environment. Based on the communicating process model, we mainly focused on establishing the formal semantics and the verification techniques of open software. The results we have achieved are listed as follows :(1) We proposed a timed extension to the communicating process model and derived an effecient alternative characterization for verification.(2) We also proposed a probabilistic extension to the communication process model and derived effecient alternative characterizations for verification.(3) We presented a general framework for "Structural Operational Semantics" specification to have the congruence and the well-definedness of "time".(4) We investigated a logical characterization of open software by the multi-autoepistemic logic.(5) We build a prototype programming environment for an efficient debugging based on the diagnostic information generation.(6) We proposed a intermidiate description that can be abstracted as a LOTOS specification and also can be expanded as a C-program at the same time.