随着计算机硬件技术与网络通信技术的快速发展,以并发性为特征的并发系统越来越显示其重要性,并已成为当前计算机软件开发的主流方向。然而由于并发系统本身所具有的复杂性,使得其开发过程难度大、效率低和周期长,很难被程序员掌握,而且开发出的软件很难避免和发现所隐含的错误和缺陷,这些问题已经成了并发系统在实际应用中的绊脚石。如何快速地获得一个正确性的并发程序,已经引起了越来越多的研究人员投身于该项研究中。传统的编程模型和编程语言,它们在表达能力或安全性方面存在着一些不足。本文紧扣这些方面,分析了当前并发编程的研究现状及其存在的问题,并结合所研项目展开了具体研究,主要针对以下几个方面进行了研究和探讨。本文首先分析了当前并发系统的重要性,阐述了PAR方法在顺序编程领域的所取得的重大成功,然而在描述并发系统上还存在不足。本文考虑在PAR方法中加入并发机制,主要是在抽象的APLA语言层上加入并发机制,使其能描述并发问题。虽然目前有许多编程语言提供对并发的支持,但大部分却对并发程序的正确性支持不够,很难保证并发程序的正确性。基于此,本文使用形式化的开发方法,完善了PAR方法的并发编程模型,在APLA语言中增加了新的语言成份,得到扩充后的APLA+语言。通过增加的语言符号,能较好的描述并发问题,并且不会出现传统并发编程中出现的等待、同步等问题。本文完整地给出了APLA+语言相关部分的语法与语义描述及相应并发编程模型通信方式---过程调用方式。针对并发程序的正确性问题,本文给出了使用seuss时序逻辑来验证APLA+并发程序的正确性性质(安全性和活性)。对于APLA+程序的安全性和活性性质,直接从APLA+程序组成的构件中推导出整个程序的性质。本文的研究表明,使用PAR方法设计一个正确性的并发程序是可行的,给出的APLA+具有严格的理论基础,能够直观准确的表达并发问题,解决现有并发程序开发难等问题,并对提高并行和并发软件的开发效率具有重要意义。