Correctness of real time systems by construction Export

@incollection{citeulike:2695793, 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.}, author = {Hooman, Jozef}, citeulike-article-id = {2695793}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-58468-4_158}, doi = {10.1007/3-540-58468-4_158}, journal = {Formal Techniques in Real-Time and Fault-Tolerant Systems}, keywords = {bpel, channel-passing, choreography, correctness\_by\_construction, top-down, webservice}, pages = {19--40}, posted-at = {2008-04-21 13:06:12}, priority = {4}, title = {Correctness of real time systems by construction}, url = {http://dx.doi.org/10.1007/3-540-58468-4_158}, year = {1994} }

TY - CHAP ID - citeulike:2695793 L3 - citeulike-article-id:2695793 N2 - 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. JF - Formal Techniques in Real-Time and Fault-Tolerant Systems EP - 40 TI - Correctness of real time systems by construction SP - 19 KW - bpel KW - channel-passing KW - choreography KW - correctness_by_construction KW - top-down KW - webservice AU - Hooman, Jozef PY - 1994/// UR - http://dx.doi.org/10.1007/3-540-58468-4_158 ER -