中科院数学与系统科学研究院

数学研究所

计算机科学研讨班

报告人： 薛锦云 教授 (江西师范大学) 

题  目：PAR: A Practicable Formal Method and Its Supporting Platform

时  间：2019.01.09（星期三）, 16:00-17:00

地  点：数学院南楼N913室

Abstract: The use of Formal methodss can significantly improve the reliability, correctness and efficiency of software development. Although Formal methods has been invented for more than 40 years, but academia and industry do not have a unified understanding of what are Formal Methods and its essential characteristics. Formal Methods has not been recognized and widely applied by academia and industry. The authors of this paper have long been engaged in the study of the essential features of formal methods. The author proposes a new definition: Formal methods is a strict technology based on mathematics and tool support for software and hardware system, including high-level abstract specification, modeling language and different levels of model transformation tools. Based on this definition, this paper develops a practicable formal methods and its supporting platform, called PAR method and PAR platform, short for PAR. PAR consists of the following elements: requirement modeling language SNL, algorithm modeling language Radl, abstract program modeling language Apla, a set of rules for the model transformation and a set of automatic transformation tools from requirement models to algorithm models, to abstract program models and to executable programs. The goal of the transformations is to generate executable program. The elements embody 6 innovative ideas given in section 2. There are two kinds of applications of PAR. One is that many nontrivial algorithms and programs have been developed formally. Another is formal developing several safety-critical information systems.

Bio: Xue Jinyun graduated from Nanjing University with major in mathematics. He did research in the area of computer science in Cornell University as a visiting scientist from 1985 to 1988, and act as visiting professor in Santa Clara University, from 1995 to 1996. In 2000 and 2009 respectively, he was engaged as the PhD supervisor by Institution of Software, Chinese Academy of Science and Wuhan University. He has been serving as the director and professor of State International S&T Cooperation  Base  of  Networked Supporting Software and Provincial Key Laboratory of High-Performance Computing. Xue started to enjoy State Council Special Contributions Allowance from 1992. He was named as “Middle-aged Expert Who had Made Nationally Outstanding Contributions” in 1996 and "Distinguished Teacher of Jiangxi Province". In recent years, he was appointed as evaluation experts in the National Outstanding Youth Fund, the National Innovation Team, State Key Laboratory, National 863 Project and Natural Science Foundation of China. Xue and his group developed PAR method and PAR platform. The preliminary achievements won the First-level Prize of Science and Technology Progress Award of Jiangxi Province.

薛锦云 南京大学数学系本科毕业， 85年-88年在美国康奈尔大学计算机系 Gries, D.  团队进修科研，95年-96年在美国Santa Clara大学做客座研究员,于2000年和2009年分别被中科院软件所和武汉大学评聘为博士生导师。现任国家网络化支撑软件国际科技合作基地和江西省高能计算重点实验室主任。他曾获“国家级有突出贡献中青年专家”称号,是享受国务院特殊贡献津贴专家，江西省“赣鄱英才555工程”领军人才,江西省首批由中共中央直接联系和掌握的高级专家。薛锦云还担任全国理论计算机科学专委会副主任和中国服务贸易协会专家委员会副理事长，还是国家杰出青年基金，国家创新团队，国家重点实验室和国家自然科学基金重点项目会评专家和会评专家组负责人。研制成功支持软件形式化和自动化开发的PAR方法和PAR平台(便捷模型驱动软件开发平台),其前期研究成果曾获江西省科技进步一等奖。