Supported by the National Science Foundation (NSF CNS award 0930225), Professor Myers in collaboration with Professor Hao Zheng of the University of South Florida extended verification methods developed for asynchronous and analog circuits to support the verification of Cyber-Physical Systems (CPS). This project developed a number of techniques for improving verification efficiency of such systems. As part of an internship with Wendelin Serwe at Inria, a student on this project, Zhen Zhang, verified a fault-tolerant NoC routing algorithm using the CADP tools. This routing algorithm was developed in collaboration with Professor Tomohiro Yoneda from the National Institute of Informatics.
Senior Personnel:
- Chris J. Myers, Professor, University of Utah
- Wendelin Serwe, Research Scientist, Inria
- Tomohiro Yoneda, Professor, National Institute of Informatics, Tokyo, Japan
- Hao Zheng, Associate Professor, University of South Florida.
Alumni:
- Kevin Jones (BS), Aberdeen Proving Ground, Philadelphia, PA.
- Robert Thacker (PhD), IBM Austin, TX.
- Jian Wu (PostDoc), Toshiba America Electronic Components, Inc., San Jose, CA, USA.
- Zhen Zhang
Software:
PhD Dissertations:
- Zhen Zhang, Verification Methodologies for Fault-Tolerant Network-on-Chip Systems , PhD Dissertation, University of Utah, May, 2016.
- Robert Thacker, A New Verification Method For Embedded Systems , PhD Dissertation, University of Utah, December, 2009.
Bachelor’s Theses:
- K. Jones, Automated Abstraction of Labeled Petri Nets, BS Thesis, University of Utah, May, 2011.
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, 2016.
- 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.
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.
- H. Zheng, A. Price, and C. Myers, Using decision diagrams to compactly represent state space for explicit model checking, in 2012 IEEE International High Level Design Validation and Test Workshop, November, 2012.
- Y. Zhang, E. Rodriguez, H. Zheng, and C. Myers, An improvement in partial order reduction using behavioral analysis, in IEEE Computer Society Annual Symp. on VLSI, August, 2012.
- H. Zheng, E. Rodriguez, Y. Zhang, and C. Myers, A compositional minimization approach for large asynchronous design verification, in 19th International SPIN Workshop on Model Checking of Software, July, 2012.
- 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.
- H. Yao, H. Zheng, and C. Myers, State space reductions for scalable verification of asynchronous designs, in 2010 IEEE International High Level Design Validation and Test Work- shop, November, 2010.
- R. Thacker, K. Jones, C. Myers, and H. Zheng, Automatic abstraction for verification of cyber-physical systems, in The 1st ACM/IEEE International Conference on Cyber-Physical Systems, April, 2010.
- R.Thacker, C. Myers, K. Jones, and S. Little, A New Verification Method For Embedded Systems, in IEEE International Conference on Computer Design, October, 2009.