Correctness of Real-Time Systems by Construction

摘要

To design distributed real-time systems in a top-down way, we present a mixedformalism in which programs and assertional specifications are combined. Specifications consist of an assumption-commitment pair, extending Hoare logic to real-time and progress properties. By defining the theory in the Prototype Verification System (PVS) specification language, the interactive proof checker of PVS can be used to reason in this framework. We show how this tool can be used during the design of real-time systems to derive programs that are correct by construction.