时间：2017年8月31日(星期四)10：40-11：30
地点：仓山校区成功楼603报告厅
主讲：华东师范大学 李钦副教授
主办：数学与信息学院
专家简介：李钦，华东师范大学计算机科学与软件工程学院副教授，2011年获华东师范大学计算机科学博士学位，导师为何积丰院士。2011-2013年担任澳大利亚昆士兰大学博士后研究员。主要研究领域为形式化方法、高可信计算，主要研究方向为程序协同语言与语义模型、高可信软件建模理论与验证方法、多智能体协同机制形式化建模与分析。已发表学术论文33篇，其中第一作者与通讯作者论文20篇，11篇为CCF C类及以上期刊与会议。承担国家自然科学基金委青年基金项目《面向时空约束的CPS协同机制的形式化建模与分析》。
报告摘要：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.