Moshe Y. Vardi William Marsh Rice University
SoD-HCER: A Theory of Automated Design
As computerized systems are becoming larger, more complex, and increasingly distributed, an increasing portion of the design effort goes into the validation and verification effort. There is a growing need for formal methods that guarantee systems reliability, correctness, and efficiency by design. This project will address this challenge by contributing to the the establishment of a theory of automated design of computing systems. The focus of this project is on moving algorithmic techniques for assertion-based automated verification into assertion-based automated design, building on emerging standard temporal assertion languages such as OVL, PSL, and SVA. The new techniques will enable the development of systems of higher quality within shorter design cycles and with lower costs. The vision for Science of Design underlying this proposal is that of design automation, in which the process of converting formal specification to implementation is, to a major extent, automated. The implication is that a major portion of the manual design effort should go into the development of high-level specification, since much of the implementation effort can then be automated. The ultimate goal of this project is a demonstrable improvement in design productivity and quality.
