Open Access. Powered by Scholars. Published by Universities.®
- Publication
- Publication Type
Articles 1 - 2 of 2
Full-Text Articles in Entire DC Network
Level Oriented Formal Model For Asynchronous Circuit Verification And Its Efficient Analysis Method, Eric G. Mercer, Tomoya Kitai, Chris Myers, Yusuke Oguro, Tomohiro Yoneda
Level Oriented Formal Model For Asynchronous Circuit Verification And Its Efficient Analysis Method, Eric G. Mercer, Tomoya Kitai, Chris Myers, Yusuke Oguro, Tomohiro Yoneda
Faculty Publications
Using a level-oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model datapath circuits. On the other hand, in order to use such a model on large circuits, techniques to avoid the state explosion problem must be developed. This paper first introduces a level-oriented formal model based on time Petri nets, and then proposes its partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.
A Formal Method To Analyze Framework-Based Software, Trent N. Larson
A Formal Method To Analyze Framework-Based Software, Trent N. Larson
Theses and Dissertations
Software systems are frequently designed using abstractions that make software verification tractable. Specifically, by choosing meaningful, formal abstractions for interfaces and then designing according to those interfaces, one can verify entire systems according to behavioral predicates. While impractical for systems in general, framework-based software architectures are a type of system for which formal analysis can be beneficial and practical over the life of the system. We present a method to formally analyze behavioral properties of framework-based software with higher-order logic and then demonstrate its utility for a significant, modern system.