Xue-Yang ZHU

Ph.D, Associate Research Professor

Institute of Software, Chinese Academy of Sciences

4th South Fourth Road, Zhongguancun, P.O.Box 8718, Beijing, P. R. China, 100190

zxy[at]ios.ac.cn

 

Research Interests

Design of Embedded Systems, Formal Methods, Smart Contracts, etc.

 

Publications and Reports

Journal Publications

1.       Pengfei Sun, Xue-Yang Zhu and Ya Gao. Optimal Offloading for Streaming Applications in Mobile Edge Computing. Journal of Circuits, Systems, and Computers (JCSC) Vol 31 No. 6, April 2022. (pdf,doi).

2.       Xue-Yang Zhu, Marc Geilen, Twan Basten, and Sander Stuijk. Multi-Constraint Static Scheduling of Synchronous Dataflow Graphs via Retiming and Unfolding. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems. 2016, 35(6): 905-918. (pdf, doi).

3.       Xue-Yang Zhu, Twan Basten, Marc Geilen, and Sander Stuijk. Efficient Retiming of Multirate DSP Algorithms. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 2012, 31(6): 831-844. (pdf, doi).

4.       Jian Zhang, Wenhui Zhang, Naijun Zhan, Yidong Shen, Haiming Chen, Yunquan Zhang, Yongji Wang, Enhua Wu, Hongan Wang, Xueyang Zhu. Basic research in computer science and software engineering at SKLCS. Frontiers of Computer Science in China. 2008, 2(1):1-11. (pdf, doi)

In Chinese with English abstract:

5.         ZHAO Ying-Qi, ZHU Xue-Yang, LI Guangyuan, Bao Yu-Long. Time Constraint Patterns of Smart Contracts and Their Formal Verification. Ruan Jian Xue Bao/Journal of Software, accepted (in Chinese). 2022,33(8).  (pdf, doi)
赵颖琪,朱雪阳,李广元,包玉龙.智能合约的时间约束模式及其形式化验证.软件学报,2022,33(8):0

6.         ZHU Xueyang. Formal analysis of the DAO exploit. Information Technology and Network Security. 2021(05): 13-19.
朱雪阳.The DAO事件的形式化分析.信息技术与网络安全, 2021(05): 13-19.

7.       BAO Yulong, ZHU Xueyang, ZHANG Wenhui, SUN Pengfei, ZHAO Yingqi. Formal verification of smart contract for access control in IoT applications. Journal of Computer Applications, 2021, 41(4): 930-938. (3rd CCF China Blockchain Conference, CBCC 2020, Jinan, China, December 18-20). (doi)
包玉龙, 朱雪阳, 张文辉, 孙鹏飞, 赵颖琪. 物联网应用中访问控制智能合约的形式化验证. 计算机应用, 2021, 41(4): 930-938. (2020 CCF中国区块链技术大会)

8.       ZHAO Yingqi, ZHU Xueyang, LI Guangyuan, GAO Ya, BAO Yulong. Verification of Smart Contracts with Time Constraints. Journal of Applied Sciences, 2021, 39(1): 1-16. (3rd CCF China Blockchain Conference, CBCC 2020, Jinan, China, December 18-20). (doi)
赵颖琪, 朱雪阳, 李广元, 高雅, 包玉龙. 带时间约束的智能合约验证[J]. 应用科学学报, 2021, 39(1): 1-16. (2020 CCF中国区块链技术大会.)

9.       Jian Liu, Purui Su, Min Yang, Liang He, Yuan Zhang, Xue-Yang Zhu, Huimin Lin. Software and Cyber Security-A Survey. Ruan Jian Xue Bao/Journal of Software, 2018, 29(1):42-68. (pdf, doi)
刘剑,苏璞睿,杨珉,和亮,张源,朱雪阳,林惠民.软件与网络安全研究综述.软件学报, 2018,29(1):42-68.

10.  Xue-Yang Zhu. A Model-Based Performance Analysis Framework for Embedded Systems. Journal of Software, 2016, 27(Suppl.(2)):328-335. (ESTC 2016. Shanghai, 29-30, Oct. 2016.) (pdf).
朱雪阳. 基于模型的嵌入式系统性能分析框架. 软件学报,2016,27(S2):328-335. (第十四届全国嵌入式系统学术会议(ESTC 2016), 上海，2016年10月29-30日.)

11.  Yu-Lei Gu, Xue-Yang Zhu, Rongjie Yan and Guangquan Zhang. Pareto Optimization and Scheduling of Synchronous Dataflow Graphs on a Heterogeneous Multicore Platform. Computer Science, 2015,42(11):43-47. (10th National Annual Conference on High Performance Computing (HPC China 2014). Guangzhou, China. 6-8 Nov., 2014. )
顾玉磊,朱雪阳,晏荣杰,张广泉.基于异构多核平台的同步数据流图帕累托优化与调度[J].计算机科学,2015, 42(11):43-47. (第十届全国高性能计算学术年会(HPC China 2014),广州,11月6-8号.)

12.  Yesheng Chai, Xue-Yang Zhu, Rongjie Yan, and Guangquan Zhang. MARTE Models based System Reliability Prediction. Computer Science,2015,42(12):82-86, 91. (13th National Software Application Conference (NASAC 2014). Guilin, China, 7-9, Nov., 2014.)
柴叶生,朱雪阳,晏荣杰,张广泉.基于MARTE模型的系统可靠性预测[J].计算机科学,2015,42(12):82-86, 91. (第十三届全国软件与应用学术会议(NASAC2014),广西桂林,11月7-9号.)

13.  Xueyang Zhu. The Dual Software Architecture Description Framework XYZ/ADL. Computer Research and Development, 2007, 44(9): 1485-1494. (pdf)
朱雪阳. 双重软件体系结构描述框架XYZ/ADL. 计算机研究与发展. 2007, 44(9)，1485~1494

14.  Xue-Yang Zhu, and Zhi-Song Tang. Compositional Semantics and Refinement of Statecharts. Journal of Software, 2006, 17(4): 670-681. (pdf)
朱雪阳, 唐稚松. Statecharts的组合语义与求精. 软件学报. 2006,17(4): 697~708.

15.  Xue-Yang Zhu, and Zhi-Song Tang. A temporal logic semantics for UML activity diagrams. Journal of Computer Research and Development, 2005, 42(9): 1478-1484. (pdf)
朱雪阳, 唐稚松.UML活动图的时序逻辑语义.计算机研究与发展. 2005,42(9):1478~1484.

16.  Xue-Yang Zhu, and Zhi-Song Tang. A temporal logic-based software architecture description language XYZ/ADL. Journal of Software, 2003, 14(4): 713-720. (pdf)
朱雪阳,唐稚松. 基于时序逻辑的软件体系结构描述语言XYZADL. 软件学报. 2003,14(4): 713~720.

Conference Publications

17.  Xufeng Zhao, Qiuyang Wei, Xue-Yang Zhu, Wenhui Zhang. Template-Based Smart Contract Verification: A Case Study on Maritime Transportation Domain. In Proc. Of the 28th International Conference on Engineering of Complex Computer Systems (ICECCS 2024). 19-21 June, 2024. Limassol, Cyprus. LNCS, vol 14784. Springer, Cham. (pdf, doi)

18.  Xufeng Zhao, Qiuyang Wei, Xue-Yang Zhu, Wenhui Zhang. A Smart Contract Development Framework for Maritime Transportation Systems, 2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security Companion (QRS-C), Chiang Mai, Thailand, 2023, pp. 310-319. (pdf, doi)

19.  Qiuyang Wei, Xufeng Zhao, Xue-yang Zhu, Wenhui Zhang. Formal Analysis of IBC Protocol. The 31st IEEE International Conference on Network Protocols (ICNP 2023). Reykjavik, Iceland, October 10-13, 2023. (pdf, doi)

20.  Yulong Bao, Xue-Yang Zhu, Wenhui Zhang, Wuwei Shen, Pengfei Sun and Yingqi Zhao. On Verification of Smart Contracts via Model Checking. Y. Aït-Ameur and F. Crăciun (Eds.): TASE 2022, LNCS 13299, pp. 1–21, 2022. (pdf, doi)

21.  Ya Gao, Wenhui Zhang, Xue-Yang Zhu. Multi-Agent Automata and Its Application to LDLK Satisfiability Checking.The 21st IEEE International Conference on Software Quality, Reliability and Security. 6-10 Dec. 2021. (doi)

22.  Wenhui Zhang, Xue-Yang Zhu and Yulong Bao.VERDS: Modeling and Verification of Finite State Systems with Discrete Time Models by Symbolic Techniques. In Proc. Of the 2021 International Symposium on Theoretical Aspects of Software Engineering (TASE 2021). 25-27 Aug. 2021. (doi)

23.  Xue-Yang Zhu. Efficient Retiming of Unfolded Synchronous Dataflow Graphs. In Proc. Of the 24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019). Guangzhou, China. 10-13 Nov. 2019, pp. 134-143. (pdf, doi)

24.  Xue-Yang Zhu. Equivalence of Transformations of Synchronous Data Flow Graphs: Work-in-Progress. In Proc. of the 23th IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis Companion (CODES/ISSS 18 Companion, part of ESWEEK 2018), Torino, Italy, Sept. 30 -October 5, 2018. Article No.11. (pdf, doi, poster)

25.  Xue-Yang Zhu. Efficient Algorithm for the Iteration Period Computation of Unfolded Synchronous Dataflow Graphs. In Proc. of the 12th International Symposium on Theoretical Aspects of Software Engineering (TASE 2018). Guangzhou, China, August 29-31, 2018. Pp.36-43. (pdf, doi)

26.  Xue-Yang Zhu. A Unified Framework for Throughput Analysis of Streaming Applications under Memory Constraints. In Proc. Of the 22nd International Conference on Engineering of Complex Computer Systems (ICECCS 2017). Fukuoka, Japan, 6-8 Nov., 2017. Pp.128-137. (pdf, doi)

27.  Xue-Yang Zhu. A Unified Framework for Throughput Analysis of Synchronous Data Flow Graphs under Memory Constraints: Work-in-Progress. In Proc. of the 22th IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis Companion (CODES/ISSS 17 Companion, part of ESWEEK 2017), Seoul, Republic of Korea, October 15C20, 2017. Article No. 2. (pdf, doi, poster)

28.  Yu-Lei Gu, Xue-Yang Zhu, Guangquan Zhang, Yifan He. Pareto Optimal Scheduling for Synchronous Data Flow Graphs on Heterogeneous Multiprocessor. In Proc. Of the 21st International Conference on Engineering of Complex Computer Systems (ICECCS 2016). Dubai, UAE, 6-8 Nov., 2016. (pdf, doi)

29.  Yu-Lei Gu, Xue-Yang Zhu and Guangquan Zhang. Pareto Optimal  Scheduling of Synchronous Data Flow Graphs via Parallel Methods. In Proc. Of the 1st International Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2015). Nanjing, China, 4-6 Nov., 2015. LNCS, vol. 9409, pp.217-223. (pdf, doi)

30.  Xue-Yang Zhu, Rongjie Yan, Yu-Lei Gu, Jian Zhang, Wenhui Zhang and Guangquan Zhang. Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking. In Proc. Of the 20th International Symposium on Formal Methods (FM 2015). Oslo, Norway, 24-26 June, 2015.  LNCS, vol. 9109, pp. 551C569, 2015. (pdf, doi)

31.  Gaogao Yan, Xue-Yang Zhu, Rongjie Yan, and Guangyuan Li. Formal Throughput and Response Time Analysis of MARTE Models. In Proc. of the 16th International Conference on Formal Engineering Methods (ICFEM 2014), LNCS, vol. 8829, pages 430-445, Luxembourg, 3-7 November, 2014. (pdf, doi)

32.  Xue-Yang Zhu, Marc Geilen,  Twan Basten,  and Sander Stuijk. Memory-Constrained Static Rate-Optimal Scheduling of Synchronous Dataflow Graphs via Retiming. In Proc. Of the 17th Design, Automation and Test in Europe (DATE2014), Dresden, Germany, 24-28 March, 2014. (pdf, doi)

33.  Xue-Yang Zhu,  Marc Geilen,  Twan Basten,  and Sander Stuijk. Static Rate-Optimal Scheduling of Multirate DSP Algorithms via Retiming and Unfolding. In Proc. Of the 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012, part of CPS Week 2012), pages 109-118. Beijing, China, 16-19 April 2012. (pdf, doi)

34.  Xue-Yang Zhu. Retiming Multi-Rate DSP Algorithms to Meet Real-Time Requirement, In Proc. Of the 13th Design, Automation and Test in Europe (DATE 2010), pages 1785 - 1790. Dresden, Germany, 8-12 March, 2010. (pdf, doi)

Book Chapters

35.  Xue-Yang Zhu, Wenhui Zhang, Guangyuan Li, Yi Lv, and Huimin Lin. Report on Advances in Model Checking. Report on Advances in Computer Science and Technology (2011-2012). ISBN9787504660206, China Science and Technology Press, 2012.  PP169-186. (in Chinese with English abstract) (pdf)
朱雪阳,张文辉,李广元,吕毅,林惠民.模型检测发展研究.《中国科协学科发展研究系列报告--2011-2012计算机科学与技术学科发展报告》, ISBN：9787504660206,中国科学技术出版社,2012. PP169~186.

Technical Reports

36.  Jian Liu, Purui Su, Min Yang, Liang He, Yuan Zhang, Xue-Yang Zhu and Huimin Lin. Software and Cyber Security - A Survey. Technical Report, ISCAS-SKLCS-16-07, State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, 2016. (in Chinese with English abstract) (pdf)

37.  Yu-Lei Gu, Xue-Yang Zhu, Rongjie Yan and Guangquan Zhang. Pareto Optimization and Scheduling of Synchronous Dataflow Graphs on a Heterogeneous Multicore Platform. Technical Report, ISCAS-SKLCS-14-14, State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, 2014. (in Chinese with English abstract) (pdf)

38.  Xue-Yang Zhu, Rongjie Yan, Yu-Lei Gu and  Guangquan Zhang. Static Optimal Scheduling and Mapping of Synchronous Dataflow Graphs on a Heterogeneous Multiprocessor Platform with Model Checking. Technical Report, ISCAS-SKLCS-14-12, State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, 2014. (pdf)

39.  Xue-Yang Zhu. An overview of FMPA and the design of FMPAer. Technical Report, ISCAS-SKLCS-13-16, State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, 2013. (in Chinese with English abstract) (pdf)

40.  Xue-Yang ZhuMarc Geilen,  Twan Basten,  and Sander Stuijk.  Retiming Synchronous Dataflow Graphs through a State-Space Exploration. Technical Report, ISCAS-SKLCS-11-53, State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, 2011. (pdf)

Thesis

41.     Xueyang Zhu. Study on Formal Description of Software Architecture. PhD thesis. Institute of Software, Chinese Academy of Sciences, 2005. (in Chinese) (Abstract in English, Abstract in Chinese)
朱雪阳.软件体系结构形式描述研究.博士学位论文.中国科学院研究生院(软件研究所).2005年.

 

Tools

FMPAer: A formal models based performance analysis tool. Its input model is the UML MARTE model.

iDFOS: A tool for optimization and scheduling of data flow graphs.

 

Professional Services

PC Member: SETTA 2019, IDEA 2016, IDEA 2015

External Reviewer of APSEC 2011

Reviewer of IEEE Transactions on Parallel and Distributed Systems (TPDS), Transactions on Design Automation of Electronic Systems (TODAES), Journal of Systems Architecture (JSA), IEEE Transactions on Reliability, Journal of Computer Science and Technology (JCST), Journal of Algorithms and Computational Technology (JACT); Journal of Computer Research and Development (CRAD)

Reviewer for Mathematical Reviews

 

Funding

Jan. 2016 – Dec. 2019. Optimization of synchronous dataflow models. National Natural Science Foundation of China (NSF China), Grant No. 61572478. (Principal Investigator)

Jan. 2015 – Dec. 2018. The Model Checking and Controller Synthesis of Metric Interval Temporal Logic MITL. National Natural Science Foundation of China (NSF China), Grant No. 61472406, Participant (PI: Dr. Guangyuan Li).

Jan. 2015 – Dec. 2018. Shape properties and data constraints of dynamic data structures: Automated analysis and verification based on separation logic. National Natural Science Foundation of China (NSF China), Grant No. 61472474, Participant (PI: Dr. Zhilin Wu).

Sept. 2010 – Aug. 2011. State Scholarship Fund. China Scholarship Council (CSC), Grant No. 2009491149.

Jan. 2009 – Dec. 2012. Theory, techniques and tools of model checking. National Natural Science Foundation of China (NSF China), Grant No. 60833001, Participant (PI: Prof. Huimin Lin).

Jan. 2009 – Dec. 2010. Theory, techniques and tools of model checking. 863 Hi-tech Research and Development Program of China, Grant No. 2009AA01Z148, Participant (PI: Prof. Jian Zhang).

 

Links

ResearchGate

DBLP

LinkedIn

A memorial of Prof. C.S. Tang (in Chinese)