张苗苗 ZHANG MIAO MIAO 博导、研究员
电子邮件: miaomiao@tongji.edu.cn
主讲课程：
实时系统
软件工程形式化方法
研究方向：
嵌入式系统和物理信息系统的分析和验证
人工智能的形式化方法
模型学习

欢迎对模型算法、形式化方法、机器和模型学习等方面感兴趣的同学报考本实验室！
部分科研项目简介
国家自然科学基金项目“扩展的线性时段不变式的模型检验”（No.**）2015/1-2018/12，第一负责人
国家自然科学基金项目“基于构件的异构嵌入式系统的模型驱动设计”（No.**）2011/1-2013/12，第一负责人
国家自然科学基金项目“基于概率时间自动机的概率时段演算的模型检验及应用研究”（No.**）2007/1-2009/12，第一负责人
教育部留学回国人员科研启动基金
部分论文简介
Jie An, Miaomiao Zhang, etc., Model Checking Continuous-time Bounded Extended Linear Duration Invariant. Accepted byHSCC(Hybrid Systems: Computation and Control) 2018.
Quan Zu, Miaomiao Zhang,Bin Yu. "Dynamic Matchings in Left Vertex Weighted Convex Bipartite Graphs" Journal of Combinatorial Optimization, 32(1): 25-50, 2016.
Jie Liu, Jing Liu, Miaomiao Zhang, etc., A Proof-Based Method for Hybrid Systems Development Using Differential Invariants. Submitted to Frontiers of Computer Science.
Guobin Wang, Jifeng He, Jing Liu, Haiying Sun, Zuohua Ding,Miaomiao Zhang, “Safety Verification of Interconnected Hybrid Systems Using Barrier Certificates,” Mathematical Problems in Engineering, vol. 2016.
祖佺, 张苗苗, 刘静. 左侧带权凸二分图动态权值匹配. 计算机学报, 39(11), 2016.
Quan Zu, Miaomiao Zhang,Bin Yu. "Fast Dynamic Weight Matchings in Convex Bipartite Graphs" 40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015, Springer, LNCS, pp. 601-612, Milano, Italy.
Quan Zu, Miaomiao Zhang, Bin Yu. "Dynamic Matchings in Left Weighted Convex Bipartite Graphs" Frontiers in Algorithmics, FAW 2014, Springer, LNCS, vol 8497, pp 330–342, Zhangjiajie, China.
Quan Zu, Miaomiao Zhang, Jiaqi Zhu,Naijun Zhan. Bounded Model-checking of Discrete Duration Calculus. HSCC 2013 (Hybrid Systems: Computation and Control) 2013.
Ziwei Liu, Jing Liu, Jifeng He, Frédéric Mallet, Miaomiao Zhang: Formal Specification of Hybrid MARTE Statecharts. TASE 2012.
Jasper Berendsen, Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang: Formal specification and analysis of zeroconf using uppaalS. ACM Trans. Embedded 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.
Xueqiang Gong,Jing Liu, Miaomiao Zhang, Jueliang Hu. Formal analysis of services compatibility. 2009 33rd Annual IEEE International Computer Software and Applications Conference, COMPSAC 2009, pp243-248.
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.
Miaomiao Zhang,Wenzhong Qin. Parametric Analysis of an Improved Fault Tolerant System. 1st International Workshop on Harnessing Theories for Tool Support in Software, ENTCS, VOLUM 207, pp 121-136.
Dehui Du, Jing Liu,Honghua Cao, Miaomiao Zhang. BAS: A Case Study for Modeling and Verification in Trustable Model Driven Development. 2nd International Workshop on Harnessing Theories for Tool Support in Software. Electr. Notes Theor. Comput. Sci. 243, pp 69-87.
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), pp165-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, pp345-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), pp242-251. Full version available as Technical Report ICIS-R06016, ICIS, Radboud University Nijmegen, 2006.
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, pages385-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), pp280-289.
H.Bohnenkamp, H.Hermanns, Miaomiao Zhang,F. Vaandrager. Cost-Optimisation of the IPv4 Zeroconf Protocol. Proceedings of the 3rd PROGRESS Workshop on Embedded Systems, Utrecht, the Netherlands, 2002.