报告人：李钦
报告题目：MAZE: A Formal Development Approach for Multi-Agent Systems
时间：2017-08-31 (星期四) 10:40 ~ 2017-08-31 (星期四) 11:30
地点：成功楼603报告厅
主办：数学与信息学院
参加对象：计算机专业感兴趣的教师和学生
报告摘要：MAZE is an extension of the Object-Z specification language supporting the specification and development of multi-agent systems (MAS). Following recommendations from the agent-oriented software engineering community, it supports three distinct levels of abstraction: (i) the macrolevel which focusses on the system’s overall, global behaviour, independently of how the agents of the system operate and interact, (ii) the mesolevel which focusses on agent interactions, and (iii) the microlevel which focusses on the operation of individual agents. Object-Z’s high-level support for component-based specification, which is well suited to modelling MAS, is complemented in MAZE with support for action refinement to facilitate the top-down development process from the macro to micro level, and with a number of syntactic conventions aimed at abstractly specifying the low-level mechanisms required for dealing with asynchronous communication and timing constraints at the micro level. The latter are shorthands for existing Object-Z notation and so require no redefinition of Object-Z’s semantics. In this paper, we provide an overview of MAZE and illustrate its use on a non-trivial case study: a swarm robotic algorithm for self-assembly.
报告人简介：2011年毕业于华东师范大学，取得计算机科学博士学位，导师为何积丰院士。2011年至2013年担任澳大利亚昆士兰大学博士后研究员。现为华东师范大学计算机科学与软件工程学院副教授，主要研究领域为形式化方法、高可信计算等，主要研究方向为程序协同语言与语义模型、高可信软件建模理论与验证方法、多智能体协同机制形式化建模与分析等。已在形式化方法相关国际期刊与会议上发表学术论文33篇，其中第一作者与通讯作者论文20篇，11篇为CCF C类及以上期刊与会议。承担国家自然科学基金委青年基金项目《面向时空约束的CPS协同机制的形式化建模与分析》。
