个人简历

Qualifications
PhD, Software Engineering Institute, East China Normal University, China (07-12)
- Major in Technology of Computer Application
Bachelor, Department Of Mathematics, East China Normal University, China (03-07)
- Major in Information and Computational Science
工作经历
Work Experiences
Faculty member (2014 - current),
Software Engineering Institute, East China Normal University (ECNU), China
- Associate Professor (2014 - current)
Postdoc (2012-2014)
Computer Science Department, School of Computing, National University (NUS), Singapore
Fellow (2009)
International Institute for Software Technology, United Nations University (UNU), Macau
开授课程
Teaching：
Undergraduate
高等数学二 （Advanced Mathematics II）
2019-2020学年第2学期，90学时，卓越班
2018-2019学年第2学期，90学时
2017-2018学年第2学期，90学时
2016-2017学年第2学期，90学时
2016-2017学年第1学期，90学时
2015-2016学年第1学期，90学时
2014-2015学年第1学期，90学时
概率论与数理统计
2019-2020学年第1学期，54学时
2018-2019学年第1学期，54学时
2017-2018学年第1学期，54学时
2016-2017学年第1学期，54学时
2015-2016学年第1学期，36学时
2014-2015学年第2学期，36学时
科研项目
Supported By:
National Key Research and Development Program of China (2019.12-2022.11)
Science and Technology Commission of Shanghai Municipality Project (PI,2018.6-2021.5)
National Science Foundation of China (PI,2015.1-2017.12)

Dissertations
[1] Yongxin Zhao, The Theory of Signal Calculus. Software Engineering Institute, East China Normal University, May, 2012.

研究领域

"可信软件工程：智能系统、信息物理融合系统、网络协议建模与分析、汽车嵌入式软件等各类系统及软件建模、分析、验证和应用研究
形式化方法：程序统一理论、形式语义理论、形式建模与分析、形式验证、定理证明
可信人工智能：对抗攻击与防御、可解释深度学习、智能系统可信性度量、鲁棒性验证
智能驾驶研究
可信硬件设计"

近期论文

Journals：
[J14] Jianmin Jiang, Huibiao Zhu, Qin Li, Yongxin Zhao, Shi Zhang, Ping Gong, Zhong Hong:
Event-based functional decomposition. Inf. Comput. 271: 104484 (2020)
[J13] Xin Li, Jian Guo, Yongxin Zhao, Xiaoran Zhu: Formal Modeling and Verifying the TTCAN Protocol from a Probabilistic Perspective. Journal of Circuits, Systems, and Computers 28(10): 1950177:1-1950177:21 (2019)
[J12] Jianmin Jiang, Huibiao Zhu, Qin Li, Yongxin Zhao, Zhong Hong, Shi Zhang, Ping Gong:
Isolation Modeling and Analysis Based on Mobility. ACM Trans. Softw. Eng. Methodol. 28(2): 10:1-10:31 (2019)
[J11] Genwang Gou, Yongxin Zhao*, Qin li, Qiwen Xu, A Mathematical Analysis of Improved EigenAnt Algorithm. Journal of Experimental and Theoretical Artificial Intelligence, 31(2):291-309（2019）.
[J10] Ling Shi, Yongxin Zhao*, Yang Liu, Jun Sun, Jin Song Dong, Shengchao Qin, A UTP semantics for communicating processes with shared variables and its formal encoding in PVS. Formal Aspects of Computing, 2018(2):1-30.
[J9] Jianmin Jiang, Huibiao Zhu, Qin Li, Yongxin Zhao, Lin Zhao, Shi Zhang, Ping Gong, Zhong Hong, Donghuo Chen: Event-Based Mobility Modeling and Analysis. TCPS 1(2): 9:1-9:32 (2017)
[J8] Yanhong Huang, Jifeng He, Huibiao Zhu, Yongxin Zhao, Jianqi Shi, Shengchao Qin: Semantic theories of programs with nested interrupts. Frontiers Comput. Sci. 9(3): 331-345 (2015)
[J7] Jianmin Jiang, Huibiao Zhu, Qin Li, Yongxin Zhao, Shi Zhang, Ping Gong, Zhong Hong, Analyzing Event-Based Scheduling in Concurrent Reactive Systems. ACM Trans. Embedded Comput. Sys. 14(4):86:1-86:27, (2015)
[J6] Qin Li, Yongxin Zhao*, Huibiao Zhu, Jifeng He, A UTP Semantical Model for Orc Language with Execution Status and Fault Handling. Frontiers of Computer Science. pp 709-725, (2014)
[J5] Yongxin Zhao,Yanhong Huang, Qin Li, Huibiao Zhu, Jifeng He, Jianwen Li, Xi Wu, Investigating System Survivability from a Probabilistic Perspective.IEICE Transactionson Information and Systems. Vol.E97-D, No. 9. pp 2356-2370，(2014)
[J4] Yongxin Zhao, Hao Xiao, Zheng Wang, Geguang Pu, and Ting Su, The semantics and verification of timed service choreography, International Journal of Computer Mathematics, Vol 91(3): 384-402, 2014.
[J3] Xi Wu, Huibiao Zhu, Yongxin Zhao, Zheng Wang, and Si Liu, Modeling and verifying the Ariadne protocol using process algebra, Comput. Sci. Inf. Syst., Vol 10(1): 393-421, (2013)
[J2] Zheng Wang, Geguang Pu, Jianwen Li, Yuxiang Chen, Yongxin Zhao, Mingsong Chen, Bin Gu, Mengfei Yang, and Jifeng He, A novel requirement analysis approach for periodic control systems. Frontiers of Computer Science, Vol 7(2): 214-235, (2013)
[J1] Zheng Wang, Lei Zhou, Yongxin Zhao, Jing Ping, Hao Xiao, Geguang Pu, and Huibiao Zhu, Web Services Choreography Validation. Service Oriented Computing and Application. Vol 4: 291-305, (2010)
Conference & Workshops：
[C34] Yongxin Zhao, Xiujuan Zhang, Ling Shi, Gan Zeng, Feng Sheng, Shuang Liu: Towards a Formal Approach to Defining and Computing the Complexity of Component Based Software. APSEC 2019: 331-338
[C33] Yilong Yang, Wei Ke, Weiru Wang, Yongxin Zhao*: Deep Learning for Web Services Classification. ICWS 2019: 440-442
[C32] Siteng Cao, Yongxin Zhao*, Ling Shi: Software Complexity Reduction by Automated Refactoring Schema. TASE2019: 208-215
[C31] Yongxin Zhao, Xi Wu, Jing Liu and Yilong Yang, Formal Modeling and Security Analysis for OpenFlow based Networks. Proc. ICECCS 2018: 23rd International Conference on Engineering of Complex Computer Systems, Melbourne, Australia, December 12-14, 2018.
[C30] Xi Wu, Yongxin Zhao, Huibiao Zhu: Integrating a Calculus with Mobility and Quality for Wireless Sensor Networks. Proc. HASE 2016: 17th IEEE International Symposium on High Assurance Systems Engineering, Orlando, FL, USA, January 7-9, 2016: 220-227
[C29] Bo Li, Mengdi Wang, Yongxin Zhao, Geguang Pu, Huibiao Zhu, Fu Song: Modeling and Verifying Google File System. HASE 2015: 207-214
[C28] Yanhong Huang, Yongxin Zhao*, Shengchao Qin, Jifeng He: Probabilistic Denotational Semantics for an Interrupt Modelling Language. ICECCS 2015: 160-169
[C27] Yongxin Zhao, Jin Song Dong, Yang Liu, Jun Sun: Towards a Combination of CafeOBJ and PAT. Specification, Algebra, and Software 2014: 151-170
[C26] Mengdi Wang, Bo Li, Yongxin Zhao, Geguang Pu: Formalizing Google File System. PRDC 2014: 190-191
[C25] Xi Wu, Si Liu, Huibiao Zhu, Yongxin Zhao: Reasoning about Group-Based Mobility in MANETs. PRDC 2014: 244-253
[C24] Longfei Zhu, Yongxin Zhao, Huibiao Zhu, and Qiwen Xu, Towards a Modeling Language for Cyber-Physical Systems. In Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. Springer-verlag LNCS 8051, pp. 394-411, 1-3 September, 2013, Shanghai, China.
[C23] Ling Shi, Yongxin Zhao, Yang Liu, Jun Sun, Jin Song Dong, and Shengchao Qin, A UTP Semantics for Communicating Processes with Shared Variables. Proc. ICFEM 2013: 15th International Conference on Formal Engineering Methods, Springer-verlag LNCS 8144, pp. 216-231, Oct 29 - Nov 1, Queenstown, New Zealand.
[C22] Yanhong Huang, Yongxin Zhao, Jianqi Shi, and Huibiao Zhu. A Denotational Model for Interrupt-Driven Programs. Proc. ESSS2013: 2nd International Workshop on Engineering safety and Security Systems, March 18-22, 2013, Luxembourg.
[C21] Xi Wu, Si Liu, Huibiao Zhu, Yongxin Zhao, and Lei Chen, Modeling and Verifying the Ariadne Protocol Using CSP. Proc. ECBS2012: IEEE 19th International Conference and Workshops on Engineering of Computer-Based Systems, Novi Sad, Serbia, 11-13 April, 2012, pp. 24-32, IEEE Computer Society
[C20] Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu, and Shengchao Qin, Investigating Time Properties of Interrupt-Driven Programs. Proc. SBMF2012: Formal Methods: Foundations and Applications, Springer-verlag LNCS 7498, Natal, Brazil, September 23-28, 2012.
[C19] Yongxin Zhao, Longfei Zhu, Huibiao Zhu, and Jifeng He, A Denotational Model for Instantaneous Signal Calculus. Proc. SEFM2012: Software Engineering and Formal Methods - 10th International Conference, Springer-verlag LNCS 7504, pp. 126-140, 1-5 October, 2012, Thessaloniki, Greece.
[C18] Yanhong Huang, Yongxin Zhao, Shengchao Qin, Guanhuan He, and João F. Ferreira. A Timed CSP Model for the Time-Triggered Language Giotto. Proc. SEW2012: 35th Annual IEEE Software Engineering Workshop, Heraclion, Crete, Greece, October 12-13, 2012,IEEE Computer Society.
[C17] Chengcheng Wu, Yongxin Zhao, and Huibiao Zhu, Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions. Proc. UTP2012: Unifying Theories of Programming, 4th International Symposium, Springer-verlag LNCS 7681, Paris, France, August 27-28, 2012.
[C16] Xi Wu, Yue Zhang, Huibiao Zhu, Yongxin Zhao, Zailiang Sun, and Peng Liu, Formal Modeling and Analysis of the REST Architecture Using CSP. Proc. WS-FM: Web Services and Formal Methods - 9th International Workshop, Springer-verlag LNCS 7843, Tallinn, Estonia, September 6-7, 2012.
[C15] Yongxin Zhao, Zheng Wang, Hao Xiao, Jing Ping, Geguang Pu, Jifeng He, and Huibiao He, A Unifying Approach to Validating Specification-Oriented XML Constraints. Proc. HASE2011: 13th IEEE International High Assurance Systems Engineering symposium. Boca Raton, FL, USA, 10-12 Nov, 2011, pp. 33-40, IEEE Computer Society.
[C14] Jianwen Li, Zheng Wang, Yongxin Zhao, Geguang Pu, Bin Gu, and Yanxia Qi, An Event-B Interpretation for SPARDL Model. Porc. HASE2011: 13th IEEE International High Assurance Systems Engineering symposium. Boca Raton, FL, USA, 10-12 Nov, 2011, pp. 41-48, IEEE Computer Society.
[C13] Si Liu, Yongxin Zhao, Huibiao Zhu, and Qin Li, A Calculus for Mobile Ad Hoc Networks from a Group Probabilistic Perspective. Proc. HASE2011: 13th IEEE International High Assurance Systems Engineering symposium. Boca Raton, FL, USA, 10-12 Nov, 2011, pp. 157-162, IEEE Computer Society.
[C12] Yongxin Zhao,Yanhong Huang, Jifeng He, and Si Liu, Formal Model of Interrupt Program from a Probabilistic Perspective. Proc. ICECCS2011: 16th IEEE International Conference on Engineering of Complex Computer Systems. Las Vegas, USA, 27-29 April, 2011, pp. 87-94, IEEE Computer Society.
[C11] Yongxin Zhao, and Jifeng He, Towards a Signal Calculus for Event-Based Synchronous Languages. Proc. ICFEM2011: 13th International Conference on Formal Engineering Methods. Springer-verlag LNCS 6991, pp. 1-13, 26-28 October, 2011, Durham, United Kingdom.
[C10] Yanhong Huang, Yongxin Zhao, Longfei Zhu, Qi Li, Huibiao Zhu, and Jianqi Shi, Modeling and Verifying the Code-Level OSEK/VDK Operating System with CSP. Proc. TASE2011:5th IEEE International Symposium on Theoretical Aspects of Software Engineering. Xi'an, China, 29-31 August, 2011, pp. 142-149, IEEE Computer Society.
[C9] Si Liu, Yongxin Zhao, Huibiao Zhu, and Qi Li, Towards a Probabilistic Calculus for Mobile Ad Hoc Networks. Proc. TASE2011:5th IEEE International Symposium on Theoretical Aspects of Software Engineering. Xi'an, China, 29-31 August, 2011, pp. 195-198, IEEE Computer Society.
[C8] Mengying Wang, Huibiao Zhu, Yongxin Zhao, and Liu Si, Modeling and Analyzing the μTESLA Protocol Using CSP. Proc. TASE2011:5th IEEE International Symposium on Theoretical Aspects of Software Engineering. Xi'an, China, 29-31 August, 2011, pp. 247-250, IEEE Computer Society.
[C7] Yongxin Zhao, Xu Wang, and Huibiao Zhu, Towards a Pomset Semantics for a Shared-Variable Parallel Language. Proc. UTP2010: 3rd International Symposium on Unifying Theories of Programming. Springer-verlag LNCS 6445, pp. 271-285, 15-16 November, 2010, Shanghai, China.
[C6] Yongxin Zhao, Yanhong Huang, Jianwen Li, and Huibiao Zhu, Probabilistic Model of System Survivability. Proc. TASE2010:4th IEEE International Symposium on Theoretical Aspects of Software Engineering. Taipei, China, 24-27 August, 2010, pp. 193-200, IEEE Computer Society.
[C5] Yongxin Zhao, Zheng Wang, Geguang Pu, and Huibiao Zhu, A Formal Model for Service Choreography with Exception Handling and Finalization. Proc. TASE2010:4th IEEE International Symposium on Theoretical Aspects of Software Engineering. Taipei, China, 24-27 August, 2010, pp. 15-24, IEEE Computer Society.
[C4] Qin Li, Yongxin Zhao, Xiaofeng Wu, and Si Liu, Promoting Models. Proc. UTP2010: 3rd International Symposium on Unifying Theories of Programming. Springer-verlag LNCS 6445, pp. 234-252, 15-16 November, 2010, Shanghai, China.
[C3] Zheng Wang, Jianwen Li, Yongxin Zhao, Yanxia Qi, Geguang Pu, Jifeng He, and Bin Gu, SPARDL: A Requirement Modeling Language for Periodic Control System. Proc. IsoLA2010: 4th International Symposium on Leveraging Applications. Springer-verlag LNCS 6415, pp. 594-608, 18-21 October, 2010, Heraklion, Crete, Greece.
[C2] Huibiao Zhu, Yongxin Zhao, and Jifeng He, Locality-based Normal Form Approach to Linking Algebraic Semantics and Operational Semantics for an Event-driven System-level Language. Proc. ASWEC2009: 20th Australian Software Engineering Conference. Gold Cost, Australia, 14-17 April, 2009, pp. 297-306, IEEE Computer Society.
[C1] Geguang Pu, Yongxin Zhao*, Zheng Wang, Libo Feng, Huibiao Zhu, and Jifeng He, A Denotational Model for Web Service Choreography. Proc. ICDCIT2008: Distributed Computing and Internet Technology, 5th International Conference. Springer-verlag LNCS 5375, pp. 1-12, 10-12 December, 2008, New Delhi, India.
国际SCI期刊编委
Youth Associate Editor(青年副编辑)
Frontiers of Computer Science（SCI，IF：0.405）