Zhen Zhang

Electrical and Computer Engineering

College of Engineering

Utah State University

Find me at:

Reach me at:

Email: zhen.zhang AT usu DOT edu

Phone: 435-797-9068

Research Interests

My primary interest is in the modeling and verification of concurrent and stochastic systems, ranging from asynchronous systems and distributed protocols to embedded software and biological systems. I am interested in developing theories and algorithms to advance techniques in the area of formal and semi-formal methods, and their applications in system diagnosis and embedded controller and parameter synthesis.

LNT Models

I developed many formal models for a link-fault tolerant routing protocol for a two-by-two Network-on-Chip mesh. The formalism used is the process-algebraic language LNT. Here are some representative ones during the evolution of the development of this link-fault routing algorithm.

LNT Models for our FMICS'14 paper.
- counterclockwise routing architecture
- abstract 2×2 NoC routing architecture
LNT Models for our SCP (SI: FMICS'14) paper.
- concrete, livelock-free 2×2 NoC routing architecture

Journal Publications:

Z. Zhang, W. Serwe, J. Wu, T. Yoneda, H. Zheng, and C. Myers, An Improved Fault-Tolerant Routing Algorithm for a Network-on-Chip Derived with Formal Analysis, in Science of Computer Programming, 118, 24-39, March, 2016.
(Author’s version is available on the HAL open archive.)
H. Zheng, Z. Zhang, C. Myers, E. Rodriguez, and Y. Zhang, Compositional Model Checking of Concurrent Systems, in IEEE Transactions on Computers, 64(6), June, 2015.
C. Madsen, Z. Zhang, N. Roehner, C. Winstead, and C. Myers, Stochastic Model Checking of Genetic Circuits, in ACM Journal on Emerging Technologies in Computing Systems, 11(3), December, 2014.
N. Roehner, Z. Zhang, T. Nguyen, C. Myers, Generating Systems Biology Markup Language Models from the Synthetic Biology Open Language, in ACS Synthetic Biology, 4(8), 867-943, March, 2015.

Conference and Workshop Papers:

Z. Zhang, W. Serwe, J. Wu, T. Yoneda, H. Zheng, and C. Myers, Formal analysis of a fault-tolerant routing algorithm for a network-on-chip, in 19th International Workshop on Formal Methods for Industrial Critical Systems, September, 2014.
(Author’s version is available on the HAL open archive.)
J. Wu, Z. Zhang, and C. Myers, A fault-tolerant routing algorithm for a network-on-chip using a link fault model, in 2011 Virtual Worldwide Forum for PhD Researchers in Electronic Design Automation, November, 2011.
C. Madsen, C. Myers, N. Roehner, C. Winstead, and Z. Zhang, Utilizing stochastic model checking to analyze genetic circuits, in 2012 Computational Intelligence in Bioinformatics and Computational Biology, May, 2012 (best student paper).