报告简介：The falling price of computational and communication components means that they will increasingly be embedded into physical products. Verifying the designs of the resulting “cyber-physical” products is challenging for several reasons. First, closed-form solutions for the behavior of physical systems rarely exist. Second, the most natural mathematical tool for modeling cyber-physical combinations, namely, hybrid (discrete/continuous) systems, exhibit pathologies that arise in neither purely continuous nor purely discrete systems. Third, the expressivity of existing continuous dynamics formalisms is generally lower than those used by domain experts.
To address these problems, we are developing a technology called “rigorous simulation”. The back-end for rigorous simulation uses validated numerics algorithms, which compute guaranteed bounds for the precision of all solutions. We show that these algorithms can be extended to compute trajectories for some hybrid systems exhibiting Zeno behavior. Ongoing work suggests that chattering behavior can be similarly addressed. We make validated numerics more accessible to non-specialists through the use of a domain-specific language, based on hybrid ordinary differential equations, which we also extend to support partial derivatives and certain types of equational modeling. An implementation called “Acumen” has been built and used for several case studies. These include virtual testing of advanced driver assistance functions, bipedal robotics, and a range of model problems for teaching at both graduate and undergraduate levels.
报告人简介：Walid Taha，瑞典哈姆斯塔德大学计算机科学教授，美国休斯顿大学兼职研究教授。曾在查尔姆斯理工大学、耶鲁大学和莱斯大学任学术职务，在诸如ACM GPCE会议和IFIP WG等多个知名国际会议任职，曾荣获美国自然科学基金委杰出青年学者奖（NSF CAREER ）。他的研究兴趣包括软件工程、编程语言语义、建模与仿真及信息-物理系统。