A Detailed Processor Model for Verification of Real-time Applications

摘要

We describe a microprocessor model and its use for reasoning about real-time applications. The model is very detailed, and is expressed in the logic of a general-purpose theorem proving program that checks proofs. We verify mathematically that the bit vectors constituting an application cause a real-time system to have specified properties.