开题报告-进程交互消息可见性研究.docVIP

一、综述本课题的研究动态，说明选题的依据和意义 1、本课题研究动态 进程代数是关于通信并发系统的代数理论的统称。 20世纪70年代后期，英国学者RMnner和C. A.R，分别提出了通信系统演算和通信顺序进程，开创了用代数方法研究通信并发系统的先河。 此后这一研究方向兴盛不衰，出现了众多类似而又 相互区别的演算系统，如ACP(提出者J.A.Ber郎tra 和J.W.K10p)，ATp(提出者M.H即n樱y)，Meije(提出者G.Eudol，R.desi~)，LOTC6等，统称为进程代数。这些代数理论都使用通信，而不是共享存储，作为进程之间相互作用的基本手段，表现出面向分布式系统的特征。 在语法上，进程代数用一组算子作为进程的构件。算子的语义通常用结构化操作语义方法定义， 这样进程就可看成是带标号的变迁系统。进程代数 的一个显著特征是把并发性归结为非确定性，将并 发执行的进程的行为看成是各单个进程的行为的所 有可能的交错合成，即所谓交错语义。林惠民院士从事的一项工作是关于并发程序的形式语义学及形式化方法的研究。他和他的同事设计并实现了世界上第一个通用的进程代数验证工具。进程代数的实际应用离不开计算机辅助工具的支持。八十年代后期，一批进程代数验证工具应运而生（如CWB, PSF, LOTOSphere等），其共同局限性是每一工具只适用于某一特定的进程演算。这种局限性妨碍了验证工具的推广应用。如何克服这种局限性是当时国际进程代数界面临的一个重大挑战。这些验证工具无法做到通用，根本原因在于缺乏既能描述不同进程演算的语义，又能为计算机所理解的通用语言。经过对不同演算的反复比较，并考虑到在计算机上实现的可能性，他提炼出了一个元语言，用它可以描述各种进程演算的公理化语义，并且具有良好的可读性。在此基础上实现了通用的交互式进程代数验证工具PAM，只要将这个元语言描述的进程演算定义输入PAM，就得到该演算的证明器。PAM可同时接受多个不同的演算，对每个演算又可生成多个证明窗口。这是世界上第一个通用的进程代数证明工具。1993年他又利用当时刚刚取得的关于消息传送进程证明系统的理论结果，对PAM加以扩充，研制成迄今世界上唯一能对付进程消息传送的验证工具VPAM。 2、选题的依据和意义 进程指的是系统的行为，系统是展示行为的系统，特别是一个软件执行、一个机器动作，甚至一个人的动作更是如此。作为控制并发系统复杂度和保证并发系统设计正确性和服务质量的一种有效的手段，形式化方法的研究经过几十年努力，取得很大成绩，相应技术已经用到了计算机软件系统和硬件系统设计的各个方面。 软硬件等并发系统规模的不断扩大，其组成和结构越来越复杂，设计、分析和开发并发系统变得越来越困难，因此必须对系统的进程进行科学系统的表示，才能保证不断发展的系统设计与分析的需求。在进程交互中，有可见性交互和不可见性交互，本文主要研究可见性研究，并提供区分可见性研究和不可见性研究的方法。进程代数是一种形式化的描述复杂并发系统的建模工具，它是一种高层的描述语言，它是支持并发分布系统对的组合描述及其性质形式化证明的代数语言。它以代数形式来描述模型，并且为模型化的系统定义了一套完整的语法和语义。 随着计算机软硬件等并发系统规模的不断扩大，其组成和结构越来越复杂，设计、分析和开发并发系统变得越来越困难，因此必须对系统的进程进行科学系统的表示，才能保证不断发展的系统设计与分析的需求。 作为控制并发系统复杂度和保证并发系统设计正确性和服务质量的一种有效的手段，形式化方法的研究经过几十年努力，取得很大成绩，相应技术已经用到了计算机软件系统和硬件系统设计的各个方面。1、基本内容 进程之间如何进行交互，交互过程中存在的一系列问题及其解决方法，进程代数的结构化操作语义，进程之间消息传递的可见性和不可见性，找到合适的案例分析，进行研究，得出结论。形式化的方法是在20实际60年代末期为了解决“软件危机”而发展起来的，所谓的形式化方法，就是利用具有严格数学基础的刻画语言和分析技术来设计、分析、简化计算机系统。形式化方法可以简单地理解为形式化刻画和形式推理相结合的一种研究方法。形式刻画就是要明确描述索要设计的系统和其性质，通常，系统的刻画是由一种形式化语言，例如进程代数来实现，这种刻画语言具有严格的语法和语义，用来表达系统的功能行为或者内部结构等，由于形式刻画语言具有严格的语法和语义，用来表达系统的功能行为或内部结构等。因为形式刻画具有严格的数学基础，因此，消除模糊性、二义性和不完整性有利于系统的设计、分析和简化并发系统，高效的机械化的系统形式化设计、分析和简化方法就是它所追求的目标。 作为控制并发系统复杂度和保证并发系统设计正确性和服务质量的一种有效的手段，形式化方法的研究经过几十年努力，取得很大成绩，相