Scalable Co-Verification
Based on Hardware IPs and Software Component
Executive Statement
The goal of this project is to develop a component-based
approach to scalable hardware and software co-verification of embedded systems
using model checking, which unifies the concepts of hardware IPs and software
components, leverages advances in assertion-based verification, extends
effectiveness of compositional model checking for system-level co-verification,
and facilitates verification reuse.
Project Members
Past Members
- Ping Hang Cheung (M.S., Currently at Intel
Corporation)
- Dr. Guowu Yang (Post-Doc, Currently at the University of Electronic
Science and Technology of China)
Funding
Software Packages
In this project, we have developed an Embedded System
Integrated Development Environment (ESIDE). Embedded system development using
ESIDE starts with selecting a platform for embedded systems which provides the
platform-specific libraries for architectural patterns and reusable components.
Component-based co-design generates the architectural specifications of
the system and its components, which are utilized in both component-based
co-simulation and co-verification together with the platform-specific libraries.
The validated and verified designs are compiled to deployment images for both
hardware and software by the component-based co-synthesis. There are feedback
loops from co-simulation, co-verification, and co-synthesis back to co-design
for reporting design errors detected.
The co-design and co-verification tools from ESIDE are
currently available for download
here.
Conference Publications
- Nicholas T. Pilkington, Juncao Li,
and Fei Xie. ESIDE: An Integrated Development Environment for
Component-Based Embedded Systems. In Proc. of 33rd Annual International
Computer Software and Applications Conference (COMPSAC), 2009.
- Kecheng Hao and Fei Xie.
Componentizing Hardware/Software Interface Design. In Proc. of Design,
Automation and Test in Europe (DATE), 2009.
- Juncao Li, Nicholas T. Pilkington, Fei
Xie, and Qiang Liu. Embedded Architecture Description Language. In Proc. of
32st Annual International Computer Software and Applications Conference (COMPSAC),
2008.
- Juncao Li, Xiuli Sun, Fei Xie, and
Xiaoyu Song. Component-Based Abstraction and Refinement. In Proc. of 10th
International Conference on Software Reuse (ICSR), 2008.
- Juncao Li, Fei Xie, and Huaiyu Liu.
Guiding Component-Based Hardware/Software Co-Verification with Patterns. In Proc. of 33rd EUROMICRO Conference on Software Engineering and Advanced
Application (SEAA), 2007.
- Ping Hang Cheung, Kecheng Hao, and Fei
Xie. Component-Based Hardware/Software Co-Simulation. In Proc. of 10th
EUROMICRO Conference on Digital System Design (DSD): Architectures, Methods and
Tools, 2007.
- Fei Xie and Huaiyu Liu. Unified
Property Specification for Hardware/Software Co-Verification. In Proc. of
31st Annual International Computer Software and Applications Conference (COMPSAC),
2007.
- Fei Xie, Guowu Yang, and Xiaoyu Song.
Compositional Reasoning for Hardware/Software Co-Verification. In Proc. of Fourth International Symposium on Automated Technology for Verification and
Analysis, 2006.
- Fei Xie, Guowu Yang, and Xiaoyu Song.
Component-Based Hardware/Software Co-Verification. In Proc. of
Fourth ACM-IEEE International Conference on
Formal Methods and Models for Codesign (MEMOCODE),
2006.
Journal Publications
Related Publications from Previous Projects
- Fei Xie, Xiaoyu Song, Haera Chung, Ranajoy Nandi.
Translation-Based Co-Verification. In Proc.
of 3rd ACM-IEEE International Conference on Formal Methods and Models for
Codesign (MEMOCODE), 2005.
- Fei Xie, Vladimir Levin, Robert P. Kurshan, and James C.
Browne. Translating Software Designs for Model Checking.
In Proc. of 7th
International Conference Fundamental Approach to Software Engineering (FASE),
2004.
- Fei Xie and James C. Browne. Verified Systems by
Composition from Verified Components. In Proc. of 4th Joint
Meeting of the European Software Engineering Conference and ACM SIGSOFT
Symposium on Foundations of Software Engineering (ESEC/FSE), 2003.
- Fei Xie, Vladimir Levin, and James C. Browne.
ObjectCheck: A Model Checking Tool for Executable
Object-oriented Software System Designs, In Proc. of 5th
International Conference Fundamental Approach to Software Engineering (FASE),
2002.