头像

赵涌鑫

软件工程学院      

个人资料

  • 部门: 软件工程学院
  • 毕业院校: 华东师范大学
  • 学位: 工学博士
  • 学历: 研究生
  • 邮编: 200062
  • 联系电话: 上海中山北路3663号华东师范大学软件学院
  • 传真:
  • 电子邮箱: yxzhao@sei.ecnu.edu.cn
  • 办公地址: 理科大楼B座1001室
  • 通讯地址: 上海中山北路3663号华东师范大学计算机科学与软件工程学院

教育经历

Qualifications

      - Major in Technology of Computer Application

      - Major in Information and Computational Science



工作经历

Work Experiences

    • Faculty member  (2014 - current),

Software Engineering InstituteEast China Normal University (ECNU), China

     - Associate Professor  (2014 - current)

    • Postdoc (2012-2014)

Computer Science DepartmentSchool of ComputingNational University (NUS), Singapore

    • Fellow (2009)

International Institute for Software TechnologyUnited Nations University (UNU), Macau


个人简介

社会兼职

国际SCI期刊编委

Youth Associate Editor(青年副编辑) 
Frontiers of Computer Science(SCI,IF:0.405)

研究方向

Research Areas


  1. 可信软件工程:智能系统、信息物理融合系统、网络协议建模与分析、汽车嵌入式软件等各类系统及软件建模、分析、验证和应用研究

  2. 形式化方法:程序统一理论、形式语义理论、形式建模与分析、形式验证、定理证明

  3. 可信人工智能:对抗攻击与防御、可解释深度学习、智能系统可信性度量、鲁棒性验证

  4. 自适应系统



欢迎各位同学报考我们项目组的研究生,我们急需具有良好的英语基础、较强的编程实践经验、扎实的数学功底、做事认真负责的同学加入我们的团队。



Qualifications

      - Major in Technology of Computer Application

      - Major in Information and Computational Science



Work Experiences

    • Faculty member  (2014 - current),

School of Computer Science and Software Engineering, 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


Current Students:

Master Students


1: Mufan Xiang(2021-2024)

Publications: Date2023 (CCF B),  ICECCS2022

2: Xiwei Li (2021-2024)

Publications: Caise2023(CCF B)

3: Fengyong Peng (2021-2024)

Publications: SEKE2023

4: Shuaishuai Feng (2021-2024)

Publications: SEKE2023

5: Zhenghai Cai (2022-2025)

Publications:

6. Wenzheng Yang (2022-2025)

Publication:



Alumini:

Master Students

1: Xiujuan Zhang (2016-2019)

Publication: APSEC2019

2: Siteng Cao (2017-2020)

Publication:TASE2019

3: Genwang Gou (2017-2020)

Publication: JETAI2019, SEKE2020

4. Jiawei Jiang  (2018-2021)

Publication: BigDataSecurity2021, SEKE2020

5. Jin Lv: (2018-2021)

Publication: IEEE Trans. Reliab. 2021 (SCI一区), SEKE2021

6.  Zhihao Liu (2019-2022)

Publication: ISPA2021

7. Hongjian Jiang (2019-2022)

Publication: TASE2021,SEKE2021

8. Zhiming Hu (2019-2022)

Publication: SEKE2021

9. Panfeng Qiu (2020-2023)

Publication: HPCC2022

10. Weiyu Xu (2020-2023)

Publication: SEKE2022

11. Zhenheng Dong (2020-2023)

Publication: SEKE2022


Teaching:

Undergraduate

  • 高等数学二 (Advanced Mathematics II
  1. 2019-2020学年第2学期,108学时(卓越班)

  2. 2018-2019学年第2学期,90学时

  3. 2017-2018学年第2学期,90学时

  4. 2016-2017学年第2学期,90学时

  5. 2016-2017学年第1学期,90学时

  6. 2015-2016学年第1学期,90学时

  7. 2014-2015学年第1学期,90学时

  • 概率论与数理统计
  1. 2019-2020学年第1学期,54学时

  2. 2019-2020学年第1学期,54学时

  3. 2018-2019学年第1学期,54学时

  4. 2017-2018学年第1学期,54学时

  5. 2016-2017学年第1学期,54学时

  6. 2015-2016学年第1学期,36学时

  7. 2014-2015学年第2学期,36学时

  • 机器学习
  1. 2020-2021学年第1学期,36学时


招生与培养

开授课程

Teaching:

Undergraduate

  • 高等数学二 (Advanced Mathematics II
  1. 2019-2020学年第2学期,90学时,卓越班

  2. 2018-2019学年第2学期,90学时

  3. 2017-2018学年第2学期,90学时

  4. 2016-2017学年第2学期,90学时

  5. 2016-2017学年第1学期,90学时

  6. 2015-2016学年第1学期,90学时

  7. 2014-2015学年第1学期,90学时

  • 概率论与数理统计
  1. 2019-2020学年第1学期,54学时

  2. 2018-2019学年第1学期,54学时

  3. 2017-2018学年第1学期,54学时

  4. 2016-2017学年第1学期,54学时

  5. 2015-2016学年第1学期,36学时

  6. 2014-2015学年第2学期,36学时


科研项目

Supported By:

  • National Key Research and Development Program of China (2020.12-2023.11)

  • 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)


学术成果


Publications:

Journals:

[J15] Jin Lv, Yongxin Zhao*, Xi Wu, Yongjian Li, Qiang Wang: Formal Analysis of TSN Scheduler for Real-Time Communications. IEEE Trans. Reliab. 70(3): 1286-1294 (2021) (SCI一区)

[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:

[c48] Panfeng Qiu, Xi Wu, Yongxin Zhao*: Generating Natural Language Adversarial Examples Based on the Approximating Top-K Combination Token Substitution. HPCC/DSS/SmartCity/DependSys 2022: 1675-1681

[c47] Mufan Xiang, Yongjian Li*, Sijun Tan, Yongxin Zhao, Yiwei Chi: Parameterized Design and Formal Verification of Multi-ported Memory. ICECCS 2022: 33-41

[c46] Weiyu Xu, Xi Wu, Yongxin Zhao*, Yongjian Li: Formal Verification and Analysis of Time-Sensitive Software-Defined Network Architecture. SEKE 2022: 369-375

[c45] Zhenheng Dong, Yongxin Zhao*, Qiang Wang: An Information Flow Security Logic for Permission-Based Declassification Strategy. SEKE 2022: 519-524

[c44] Qiang Wang, Jiawei Jiang, Yongxin Zhao*, Weipeng Cao, Chunjiang Wang, Shengdong Li: Algorithm selection for software verification based on adversarial LSTM. BigDataSecurity 2021: 87-92

[c43] Zhihao Liu, Qiang Wang, Yongjian Li, Yongxin Zhao*: CMSS: Collaborative Modeling of Safety and Security Requirements for Network Protocols. ISPA/BDCloud/SocialCom/SustainCom 2021: 185-192

[c42] Wenhan Wu, Yongxin Zhao*, Chao Peng, Yongjian Li, Qin Li: Analyzing and Recommending Development Order Based on Design Class Diagram. KSEM 2021: 524-537

[c41] Zhiming Hu, Zheng Wang, Hongjian Jiang, Yuyuan Zhang, Yongxin Zhao: HHML: A Hierarchical Hybrid Modeling Language for Mode-based Periodic Controllers. SEKE 2021: 31-36

[c40] Yongxin Zhao, Hongjian Jiang, Jin Lv, Sijun Tan, Yongjian Li: AnB2Murphi: A Translator for Converting AliceBob Specifications to Murphi. SEKE 2021: 108-113

[c39] Hongjian Jiang, Yongjian Li, Sijun Tan, Yongxin Zhao: Encoding Induction Proof in Dafny. TASE 2021: 95-102

[c38] Shiling Feng, Xiaohong Chen, Qin Li, Yongxin Zhao: RE2B: Enhancing Correctness of Both Requirements and Design Models. TASE 2021: 191-198

[c37] Huaiwei Yang, Shuang Liu, Lin Gui, Yongxin Zhao, Jun Sun, Junjie Chen: What Makes Open Source Software Projects Impactful: A Data-Driven Approach. Internetware 2020: 126-135

[c36] Genwang Gou, Yongxin Zhao*, Jiawei Jiang, Ling Shi: The Prediction of Delay Time and Route Planning for Autonomous Vehicles. SEKE 2020: 7-12

[c35] Jiawei Jiang, Yongxin Zhao*, Xi Wu, Genwang Gou: A Detect-and-Modify Region-based Classifier to Defend Evasion Attacks. SEKE 2020: 19-24

[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.


Dissertations

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



Locations of visitors to this page


荣誉及奖励

10 访问

相关教师