您的位置:首页 > 科学研究 > 学术科研

计信院前沿学术报告(2017-09-08)

发布时间:2017-09-05 来源:本站原创 作者:本站编辑   浏览次数:

西南大学计信院前沿学术报告

Southwest University IT Faculty Seminar

报告题目:Towards A Formal Method of Software Design and Beyond

时间:2017 9 8 日(星期五)上午10:30

地点:西南大学计信院,25教十三楼1320会议室

报告人:朱鸿 教授(英国牛津布鲁克斯大学)

报告人简介:

朱鸿,1978年至1987年就读于南京大学计算机系计算机软件专业,分别于19821984 1987年获得计算机软件学士、硕士和博士学位。19871998年在南京大学软件研究所、计算机系任教,1996年评聘为教授、博士生导师,期间于1990年至1994年访问英国Brunel University Open University,任研究员。1998年至今在英国牛津布鲁克斯大学(Oxford Brookes University)任教,现任教授,博士生导师,领导Applied Formal Methods研究组, IEEE资深会员,ACM和英国计算机学会会员。1997年获得国家杰出青年基金项目,2000年获国防科技大学长江学者特聘教授。近年来主要从事软件工程和云计算的研究工作,包括针对云软件的形式化方法、软件设计、软件测试与质量保证、软件语言等方向。曾主持或参加多项863973科研课题、自然科学基金重大课题和国防科学基金研究项目的研究。著有专著两部、学术论文190余篇。任《Journal of Software Testing, Verification and Reliability》、《Software Quality Journal》、《Multi-Agent and Grid Systems-International Journal》、《软件学报》等学术刊物编委。曾主持和参加了多项863973科研课题、自然科学基金重大课题和国防科学基金研究项目的研究。曾获得教育部优秀年轻教师奖励基金、霍英东青年教师奖二等奖(研究类)等奖励。

内容摘要:

   软件设计能否形式化?在本次讲座中我会报告我们在发展软件设计形式化方法方面的一系列尝试。我们的工作基于现有的面向模式的(pattern-oriented)软件设计方法,从对面向对象软件设计模式的形式化出发。该方法利用谓词逻辑对面向对象设计模式的结构和行为特征进行描述。我们的第二项工作是关于模式的组合。我们定义了关于模式的六个算子,从而可以对模式组合和实例化进行形式化描述。我们证明了这些算子满足的一组完全的代数规则集,从而可以证明面向模式设计之间的等价关系。我们的第三项工作是关于设计模式可组合性的形式化研究。我们提出了特征保持语义保持正确性保持的概念,以作为有效模式组合的判别准则。我们证明了关于有效模式组合的一系列结论,使得模式组合的有效性可以被形式化地证明, 且该证明可以通过定理证明器自动完成。最后,关于模式作为可重用知识,我们探讨了所提模式理论的推广,以使其成为一种通用的形式化知识表示方式,从而应用于非面向对象软件领域,例如安全设计、艺术设计、网络空间模式等。能否利用模式建立机器学习同符号推理之间的链接?能否利用模式使机器学习结果可理解、可确认、可测试、可重用?还有许多问题有待讨论。