时间：2017年8月31日(星期四)9：30-10：30
地点：仓山校区成功楼603报告厅
主讲：华东师范大学 赵涌鑫副教授
主办：数学与信息学院
主讲简介：赵涌鑫，华东师范大学计算机科学与软件工程学院副教授，2012年获华东师范大学计算机科学博士学位，导师为何积丰院士。2012-2014年新加坡国立大学博士后。主要研究领域为形式化方法、高可信计算，主要研究方向为程序语言与语义模型、高可信软件建模理论与验证方法、CPS系统建模与分析。已发表学术论文38篇，其中第一作者与通讯作者论文15篇，18篇为CCF C类及以上期刊与会议。承担国家自然科学基金委青年基金项目《基于UTP的混成建模语言的理论研究》。
报告摘要：The signal calculus for event-based synchronous language is used for specification and programming of embedded systems, which adopts broadcasting communication and follows the so-called synchronous hypothesis. Our intention is to develop an algebra for linking semantic theories ofreactions. In this paper, we mainly investigate instantaneous signal calculus (I-calculus) which contains all conceptually instantaneous reactions, i.e., zero-time reactions. The delay-time reactions will be researched in the follow-up work. To explore the semantic definition of instantaneous signal calculus, a set of algebraic laws is provided to reduce all instantaneous reactions to a normal form algebraically, which exposes the internal implicit dependence explicitly. Consequently, that two differently written reactions happen to mean the same thing can be proved from the equations of an algebraic presentation. Based on the algebra, we give several important concepts and properties concerning the distinct features of instantaneous reactions and derive an observation-oriented denotation semantics with respect to the algebraic semantics. Thus the equality of two differently written reaction is algebraically provable if and only if the two reactions are equivalent with respect to the denotational semantics.