Abstract
To design distributed real-time systems in a top-down way, we present a mixed formalism 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 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.
Cite
CITATION STYLE
Hooman, J. (1994). Correctness of real time systems by construction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 863 LNCS, pp. 19–40). Springer Verlag. https://doi.org/10.1007/3-540-58468-4_158
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
