PAR平台中算法程序模型变换正确性研究

PAR platform was software formal and automate development platform which was developed by our research team by more than twenty years of independent research and support of national research projects. PAR implemented MDD by transform Radl model to Apla model, and Apla model to executeable program model. This project will research on correctness of model tranformation in PAR platform, especially Apla model to executeable program model. The research content include verficating Apla model by Isabelle and Loop invariants semi-automatically, verifacting generic constraint by algebra structure and axiomatic semantics, ensuring the model transformation of APLA programs to executable program model is correct by generation rules and key transformation algorithm, exploring the correctness of service interaction mechanism in Apla+ model. It is expected that the final solution to ensure the correctness of the model transformation which is a very challenging and creative problem. Along our unique technical route, occupy the international high ground of high reliability software formal and automatic development as soon as possible.

PAR平台是申请者所在团队历经二十多年，在十几项国家级课题连续资助下，自主研发的软件形式化与自动化开发平台。PAR平台通过Radl程序模型变换为Apla程序模型，再变换为可执行程序模型，实现了模型驱动的软件开发。围绕PAR平台中模型变换的正确性，尤其是Apla程序模型到可执行程序模型变换过程中的正确性验证开展深入研究。重点研究利用新策略开发循环不变式，进而通过Isabelle定理证明器半自动验证Apla程序模型的正确性；通过代数结构与公理语义验证Apla程序模型中泛型约束机制的正确性；通过验证生成规则和关键变换算法，保证Apla程序模型变换为可执行程序模型的正确性；并探索Apla+程序模型中服务交互机制正确性验证问题。有望最终解决保证模型变换正确性，这一极具挑战性和创造性的问题。沿着我们特有的技术路线，尽快占领高可靠软件的形式化与自动化开发领域的国际制高点。

PAR平台是申请者所在团队历经二十多年，在十几项国家级课题连续资助下，自主研发的软件形式化与自动化开发平台。PAR平台通过Radl程序模型变换为Apla程序模型，再变换为可执行程序模型，实现了模型驱动的软件开发。.围绕PAR平台中模型变换的正确性，重点研究了利用新策略开发循环不变式，进而通过定理证明器验证Apla程序模型的正确性；验证Apla程序模型中泛型约束机制的正确性；验证Apla程序模型变换为可执行程序模型的正确性；探索Apla+程序模型中服务交互机制正确性的验证。.利用两种开发新策略为Apla程序模型开发循环不变式。结合循环不变式开发新策略取得的研究成果，Hoare公理体系、Dijkstra最弱前置谓词方法和定理证明系统的自身特点，给出用定理证明器机械化验证Apla程序模型正确的方法，并总结了验证的主要步骤。.基于一阶谓词逻辑给出基本数据类型作泛型参数，基于代数结构给出自定义抽象数据类型作泛型参数，基于公理语义给出子程序作泛型参数的约束机制。成功将上述泛型约束机制转变为Isar证明脚本，并利用Isabelle定理证明器对约束机制正确性进行验证，同时完成验证Apla程序模型变换为可执行程序模型的正确性。.成功扩展PAR平台Apla+语言（并发分布和顺序程序设计通用的语言），通过在Apla语言中扩充并行、衍生、顺序、调用和选择等五个服务交互算子，将Apla程序模型过渡到能够实现服务交互机制的Apla+程序模型。在此基础上，建立服务交互的Apla+表示到相关验证工具SMV表示的转换工具，实现服务交互程序模型的验证。.圆满完成研究计划，取得预期研究成果。在学术论文方面，发表学术论文11篇，其中学术期刊论文6篇，国际学术会议论文5篇，EI收录6篇。在学术交流方面，参加国际学术会议11人次，参加国内学术会议19人次，承办学术会议或学术活动3场。在人才培养方面，培养博士研究生2人，青年教师2人，硕士研究生8人。.