张苗苗 ZHANG MIAO MIAO    博导、研究员
电子邮件: miaomiao@tongji.edu.cn

主讲课程:
实时系统
软件工程形式化方法


研究方向:

智能系统的模型学习和验证

强化学习

人机物联网系统的软件定义

可信人工智能


欢迎对模型算法、机器和模型学习以及智能系统验证等方面感兴趣的同学报考本实验室!


部分科研项目简介

  • 国家自然基金重点项目"人机物三元融合场景的泛在计算抽象和软件定义方法”子课题负责人 2021-2025

  • 国家自然科学基金项目“时间系统的模型学习”2020/1-2023/12,第一负责人

  • 国家自然科学基金项目“扩展的线性时段不变式的模型检验”(No.61472279)2015/1-2018/12,第一负责人

  • 国家自然科学基金项目“基于构件的异构嵌入式系统的模型驱动设计”(No.61073022)2011/1-2013/12,第一负责人

  • 国家自然科学基金项目“基于概率时间自动机的概率时段演算的模型检验及应用研究”No.606030372007/1-2009/12,第一负责人

  • 教育部留学回国人员科研启动基金


部分论文简介

  • Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang: Learning real-time automata. Sci. China Inf. Sci. 64(9) (2021)

  • Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang: Inferring Switched Nonlinear Dynamical Systems. Formal Aspects Comput. 33(3): 385-406 (2021)

  • Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang: Learning Nondeterministic Real-Time Automata. ACM Trans. Embed. Comput. Syst. 20(5s): 99:1-99:26 (2021)

  • Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, Ting Gan: From model to implementation: a network algorithm programming language. Sci. China Inf. Sci. 63(7) (2020)

  • Bai Xue, Miaomiao Zhang, Arvind Easwaran, Qin Li: PAC Model Checking of Black-Box Continuous-Time Dynamical Systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11): 3944-3955 (2020)

  • Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan: PAC Learning of Deterministic One-Clock Timed Automata. ICFEM 2020: 129-146

  • Jin Xu, Zishan Li, Bowen Du, Miaomiao Zhang, Jing Liu:Reluplex made more practical: Leaky ReLU. ISCC 2020: 1-7

  • Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang: Learning One-Clock Timed Automata. TACAS (1) 2020: 444-462

  • Jie An, Lintai Wang, Bohua Zhang, Naijun Zhan and Miaomiao Zhang. Learning real-time automata. accepted by SCIENCE CHINA Information Sciences

  • Yilong Yang, Quan Zu, Wei Ke, Miaomiao Zhang, Xiaoshan Li: Real-Time System Modeling and Verification Through Labeled Transition System Analyzer. IEEE Access 7: 26314-26323 (2019)

  • Xiaoxue Hou, Jie An, Miaomiao Zhang, Bowen Du, Jing Liu: High-Speed Rail Operating Environment Recognition Based on Neural Network and Adversarial Training. ICTAI 2019: 840-847

  • Jie Liu, Jing Liu, Miaomiao Zhang, Haiying Sun, Xiaohong Chen, Dehui Du, Mingsong Chen: A proof-based method of hybrid systems development using differential invariants. Frontiers Comput. Sci. 12(5): 1026-1028 (2018)

  • Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, Wang Yi: Model Checking Bounded Continuous-time Extended Linear Duration Invariants. HSCC 2018: 81-90

  • Quan Zu, Miaomiao Zhang, Bin Yu: Fast Dynamic Weight Matchings in Convex Bipartite Graphs. MFCS (2) 2015: 601-612

  • Quan Zu, Miaomiao Zhang, Jiaqi Zhu, Naijun Zhan: Bounded model-checking of discrete duration calculus. HSCC 2013: 213-222

  • Jasper Berendsen, Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang: Formal specification and analysis of zeroconf using uppaalS. ACM Trans. Embed. Comput. Syst. 10(3): 34:1-34:32 (2011)

  • Miaomiao Zhang, Zhiming Liu, Naijun Zhan. Model Checking Linear Duration Invariants of Networks of Automata. 3rd International Conference on Fundamentals of Software Engineering, FSEN 2009, LNCS 5961, 244-259

  • Miaomiao Zhang, Zhiming Liu, Charles Morisset, Anders P. Ravn. Design and Verification of Fault-Tolerant Components .  In Methods, Models and Tools for Fault Tolerance (MEMoT 2009), LNCS 5454, 57-84.

  • Quan Zu, Miaomiao Zhang, Jing Liu, Qingfeng Du: Designing, Modelling and Verifying a Container Terminal System Using UPPAAL. 11th IEEE High Assurance Systems Engineering Symposium (HASE 2008): 445-448.

  • Miaomiao Zhang, Dang Van Hung, Zhiming Liu. Verification of Linear Duration Invariants by Model Checking CTL Properties. 5th International Colloquium on Theoretical Aspects of Computing (ICTAC 2008), LNCS 5160 , 395-409

  • Dang Van Hung, Miaomiao Zhang. On verification of probabilistic timed automata against probabilistic duration properties. Proceedings of the 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2007), pp 165-172

  • B. Gebremichael, F.W. Vaandrager, M. Zhang, K. Goossens, E. Rijpkema, A. Radulescu. Deadlock Prevention in the Aethereal Protocol. Proceedings 13th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'05), LNCS 3725, pp 345-348

  • Miaomiao Zhang, Dang Van Hung. Formal Analysis of Streaming Downloading Protocol for System Upgrading. In the proceedings of the 4th Workshop on Quantitative Aspects of Programming Languages (QAPL 06), Electr. Notes Theor. Comput. Sci. 164(3): 205-224

  • B. Gebremichael, F.W. Vaandrager, Miaomiao Zhang. Analysis of a Protocol for Dynamic Configuration of IPv4 Link Local Addresses using Uppaal. Appear in Proceedings 6th Annual ACM Conference on Embedded Software (EMSOFT 2006), pp 242-251

  • Fehnker, F.W. Vaandrager, Miaomiao Zhang. Modeling and Verifying a Lego Car Using Hybrid I/O Automata. In the book "Models, Algebras, and Logic of Engineering Software", Nato ASI Series III: Computer and Systems Sciences, Volume 191, pages 385-402, IOS Press, 2003

  • Fehnker, F.W. Vaandrager, Miaomiao Zhang. Modeling and Verifying a Lego Car Using Hybrid I/O Automata. In Third International Conference on Quality Software (QSIC 2003), pp 280-289


联系我们

地址:中国 上海曹安公路4800号同济大学软件学院

邮编:201804

联系电话:86-21-69589585,69589332(FAX)

Copyright© 2017 同济大学软件学院