——记北京大学数学科学学院副教授孙猛

本刊记者  李 刚

提起数学，是令许多人颇为头疼的一门学科：枯燥、乏味似乎为其无形中做了一种隐形的“代言”，但对北京大学数学科学学院副教授孙猛来说，却甘之如饴。他所研究的数学也绝非仅限于基础数学，在信息科学领域造诣颇深的孙猛一直致力于将数学引入另一片天地。

数学中的奇思妙想

　　自从接触到数学，孙猛就将数学视为自己不可分割的一部分，在和孙猛交谈的短短一个多小时中，记者看到了他身上承载着的对于科研的严谨、教学的负责，更了解了他背后不为人知的辛劳和快乐。

　　1994年，年仅15岁的孙猛被北京大学技术物理系录取，一年后转入数学系（现数学科学学院）学习。而20世纪90年代后期正是信息科学技术飞速发展的一个阶段，其中许多问题的解决都需要深厚的数学背景，在本科期间的学习过程中，孙猛的兴趣逐渐从纯粹的数学理论转向了数学与信息科学的交叉领域。1999年，孙猛获得推免资格，保送成为应用数学专业硕士生，刚刚步入一个新天地的孙猛又走到了一个“十字路口”。据孙猛回忆，他研究生的导师张乃孝教授所研究的主要领域为语言相关的问题，包括程序语言及领域语言等，但经过一段时间的学习了解后，孙猛发觉自己真正更感兴趣的问题还是集中在数学在信息科学之中的应用。所幸，导师给予了他充分的学术自由，鼓励他自己找寻研究方向，并在2002年孙猛选择继续攻读博士学位后推荐他去联合国大学国际软件技术研究所（UNU/IIST）交流。在UNU/IIST期间，孙猛和来自奥地利Graz工大的Bernhard Aichernig教授等合作，开始了关于组件技术的余代数理论基础的研究工作。

　　从20世纪90年代中后期开始，在计算机领域对余代数理论及其在并发模型、面向对象、模态逻辑、自动机理论等问题中的应用的研究得到了飞速发展。荷兰CWI的Jan Rutten教授提出的泛余代数理论将计算机科学中许多不同的具体行为进行抽象，得到了统一的余代数模型。在深入了解了这一理论之后，孙猛发现其基于观察的行为描述与软件组件的“黑盒”特性极其相符，非常适于作为软件组件的理论模型，并决定以此作为其博士论文的主题。孙猛在其博士论文中所提出的在余代数框架下的组件精化理论受到了国际同行和相关领域专家的高度评价，发表在第10届代数方法和软件技术国际会议上（AMAST 2004）的论文被评为该会议唯一一篇“Best Student Paper”。

　　而统一建模语言（UML）作为被广泛接受的工业标准，已经成为全世界大学和各种专业培训项目中计算机科学及工程课程中必不可少的一部分，其最主要的设计目标是使其成为一个通用的建模语言，可供不同领域使用。“但在模型不一致的情况下，很容易因模型的冲突而导致最后实现的错误，所以需要对UML中不同的视图模型给出一个精确的统一形式化语义，能够在此基础上检查不同模型的一致性，这对代码的自动生成以及开发后期的系统测试、维护等工作都会有很大帮助。”孙猛补充道。在他的博士论文及其后续工作中，孙猛对UML中的类图、状态机图、顺序图、用例图等多种常用视图模型使用余代数给出了一种统一的语义定义框架，并在此基础上成功给出了UML模型的精化、重构等操作的定义及证明方法。

复杂系统中的协调

　　随着网络技术的飞速发展，为保证系统在动态的开放分布式环境中顺利运行，系统各组件之间以及软硬件之间都需要进行紧密协调工作。如今，协调模型和协调语言在计算机科学中已经得到了广泛应用。在获得博士学位并于新加坡国立大学计算学院从事了1年的博士后研究之后，孙猛于2006年受到荷兰数学与计算机科学研究中心(CWI)的Farhad Arbab教授邀请加入其课题组，开始从事关于协调模型和语言的研究工作。十余年来，孙猛一直关注着协调模型和协调语言领域，协调模型的自动生成、验证与测试、协调模型的扩展以及相关工具的开发等是他目前研究的重点问题。

　　欧洲科学院院士Christel Baier等在2005年提出了一种从自动机规范自动生成连接件的方法，但一方面复杂系统的自动机规范难以直接给出，另外该方法的结果中存在大量冗余的异步通道，从而导致状态空间过大，难以对系统进行有效验证。孙猛与Christel Baier和Farhad Arbab合作，提出了一种从UML的顺序图自动生成协调模型的结构化方法，成功克服了这两个方面的问题，并且给出了该生成方法的正确性证明，这一证明通过给出生成的连接件和UML顺序图两者的余代数语义之间的互模拟关系，保证了生成结果和顺序图规范之间的语义的一致性。

　　通过研究基于协调语言Reo的协调机制的理论基础，以不同软硬件组件之间的交互问题以及对组件交互行为进行组合和协调的连接件所支持的系统体系结构为对象，孙猛及其团队与国际同行合作，将Reo语言进行了多种扩展：通过增加概率和随机行为相关信息，定义了Reo的定量扩展，并成功实现了从定量Reo到连续时间马尔科夫链的变换，从而可对相关的概率时序逻辑所描述的性质进行验证；在主持的国家自然科学基金青年基金项目“基于Reo的协调理论及其在信息物理系统开发方法中的应用”中，通过将微分方程与协调语言的结合，建立了信息物理系统中的连接件形式化模型，并且对信息物理系统中连接件的建模、分析、验证和测试的理论与方法进行了研究，这可谓是对信息物理系统的设计和开发搭了一架便利“桥梁”，也为具有复杂结构的信息物理系统的建模、分析和严格开发提供了更好的理论和方法支持。同时，对混成连接件的可组合性、连接件的测试用例生成方法等相关问题都进行了研究，得到了一系列的成果。

　　“早在上世纪90年代，协调语言的概念就已经被提出，这一问题多年来一直是国际上科学工作者的研究热点，也引起了包括生物信息学、面向服务计算等众多相关领域的关注。但万物皆不完美，在研究中，我们认识到，虽然协调问题的研究在国际上是一个不断发展的领域，也已经取得了一些成果，但是距离实际系统，特别是信息物理系统开发的需要还有很大差距，仍有很多问题亟待研究和解决。”孙猛如是说道。

　　在科研这条长满鲜花又布满荆棘的道路上，无论时光荏苒，孙猛始终不忘初心，一路砥砺前行。