基于模型驱动的并发建模语言Apla+设计及其可靠性研究

With rapid development and application of cloud-computing, concurrent and distributed computing become more and more important. However, it is generally accepted in academic and industry domain that the theory and techniques of concurrent and distributed computing are more complicated, variable and difficult to control. Finding a simple and reliable concurrent language mechanism has become a new challenge for software industry. Based on our original research achievement - abstract sequential programming language Apla from PAR method/PAR Platform, the applicant will do intensive research on the following aspects. Firstly, a simple, useful and dependable concurrent mechanism is developed. The Apla+ programming language is proposed with the implementation of this mechanism in Apla programming language. Secondly, using the idea of Model-Driven Development (MDD), an refinement algorithm, converting Apla+ abstract program (Platform-Independent Model) into Java executable program (Platform-Specific Model), will be designed. The tool,called Apla+ToJava Generator, will support the automatic translation from Apla+ program to Java program. Finally, a correct framework of the platform and concurrent mechanism will be proved by using category theory. The saftey and liveness of Apla+ concurrent program will be verified via Isabelle auotmatic prover. In summary, the simple and convenient concurrent language Apla+ and its supporting platform (Apla+ToJava Generator) could greatly promote the development of programming languages, especially simplify concurrent programming and improve the efficiency of concurrent programming.

云计算的推广和应用对并发分布式计算提出了越来越高的需求。学术界与工业界均普遍认为并发计算的理论和技术复杂、多变、难以掌控。寻求便捷可靠并发语言机制的研究正在悄然掀起。本项目试图以申请者所在科研团队自主研发的原创性研究成果--PAR方法/PAR平台的抽象顺序程序设计语言Apla为基础，设计简单、易用和可靠的并发语言机制；并与现有Apla语言融合，使之成为兼顾并发和顺序的通用抽象建模语言Apla+。基于模型驱动开发(MDD)技术，研究将Apla+抽象程序(PIM模型)转换为Java程序(PSM模型)的精化算法，构造Apla+ToJava自动生成系统。最后，利用范畴理论构建整个系统的正确性架构，使用Isabelle定理证明器验证Apla+抽象并发程序的安全性和活性。Apla+语言及其支撑平台将大幅度提高并发软件质量和开发效率，简化并发程序设计的难度，有助于开发人员摆脱传统并发编程的困惑和恐惧。

云计算和大数据的迅速发展对并发计算提出了越来越高的要求。学术界与工业界均普遍认为：与传统的顺序程序设计相比，并发计算的理论和技术复杂、多变、难以掌控。究其根源，除了并发计算本身的间断性、非确定性、异步性、互斥和同步之外，通用程序设计语言（如Java、C#、C++、Python等）的并发机制使用复杂、繁琐，导致程序员的开发过程难度大、效率低、周期长，而且还很难避免或发掘其中隐含的错误和缺陷。.针对上述问题，本项目在寻求便捷可靠的并发语言机制上开展了有理论价值和实践意义的研究。研究内容包括如下三个方面：(1)基于课题组所在科研团队原有的研究成果——PAR方法/PAR平台的抽象顺序程序设计语言Apla，借鉴并发模型研究领域的先驱者、美国工程院院士、德克萨斯大学奥斯汀分校Jayadev Misra教授的结构化并发语言Orc，设计出简单易用的五个调度算子(并行、衍生、顺序、剪裁和选择)和并发执行单元Bundle。将该并发机制与顺序语言Apla相融合升级成为同时支持并发和顺序设计的通用抽象建模语言Apla+。(2) 基于模型驱动开发(Model-Driven Development)技术，选择Java作为目标语言，提出了将Apla+抽象程序(Platform-Independence Model)转换为Java程序(Platform-Specific Model)的精化算法，构造出Apla+2Java自动生成原型系统。(3) 使用Isabelle和Coq定理证明器验证对并发程序的安全性和活性进行了探索性研究。基于Lipton的约简理论，提出了三种对并发程序的可线性化(Linearizability)的判断方法：基于抽象的单路约简方法、基于抽象的双路约简方法和松散约简方法，并通过11个实例证明了这些方法的合理性和适用性。.关键数据包括如下：并发执行单元Bundle的语法、语义和语用；5类调度算子的语法、语义和语用；Apla+2Java原型系统内的代码；并发程序和构件形式化验证的代码。.研究意义：本项目设计的Apla+并发机制的特点是抽象层次高，有助于编程员摆脱传统并发编程的困惑和恐惧，具有学术价值。本项目研发的Apla+2Java原型系统能够提高并发开发效率，简化并发程序设计的难度。课题组将该原型系统应用到科研、教学、软件系统开发和软件服务外包等领域。