The existence of refinement mappings Export

@inproceedings{citeulike:3321474, abstract = {Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. The authors consider specifications consisting of a state machine (which may be infinite-state) that specifies safety requirements and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a lower-level specification S₁ to higher-level one <e1>S</e1>₂ is a mapping from <e1>S</e1>₁'s state space to <e1>S</e1>₂'s state space that maps steps of S₁'s state machine steps to steps of <e1>S</e1>₂'s state machine and maps behaviors allowed by S ₁ to behaviors allowed by <e1>S</e1>₂. It is shown that under reasonable assumptions about the specifications, if <e1>S</e1>₁ implements <e1>S</e1>₂, then by adding auxiliary variables to <e1>S</e1>₁ one can guarantee the existence of a refinement mapping. This provides a completeness result for a practical hierarchical specification method}, author = {Abadi, M. and Lamport, L.}, booktitle = {Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on}, citeulike-article-id = {3321474}, citeulike-linkout-0 = {http://dx.doi.org/10.1109/LICS.1988.5115}, citeulike-linkout-1 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5115}, doi = {10.1109/LICS.1988.5115}, journal = {Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on}, keywords = {automata-theory, for--nafe, formal-logic, have-paper-copy, interesting-rating--3}, pages = {165--175}, posted-at = {2008-09-23 13:43:24}, priority = {0}, title = {The existence of refinement mappings}, url = {http://dx.doi.org/10.1109/LICS.1988.5115}, year = {1988} }

TY - CONF ID - citeulike:3321474 L3 - citeulike-article-id:3321474 N2 - Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. The authors consider specifications consisting of a state machine (which may be infinite-state) that specifies safety requirements and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a lower-level specification S₁ to higher-level one <e1>S</e1>₂ is a mapping from <e1>S</e1>₁'s state space to <e1>S</e1>₂'s state space that maps steps of S₁'s state machine steps to steps of <e1>S</e1>₂'s state machine and maps behaviors allowed by S ₁ to behaviors allowed by <e1>S</e1>₂. It is shown that under reasonable assumptions about the specifications, if <e1>S</e1>₁ implements <e1>S</e1>₂, then by adding auxiliary variables to <e1>S</e1>₁ one can guarantee the existence of a refinement mapping. This provides a completeness result for a practical hierarchical specification method JF - Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on EP - 175 TI - The existence of refinement mappings T2 - Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on SP - 165 KW - automata-theory KW - for--nafe KW - formal-logic KW - have-paper-copy KW - interesting-rating--3 AU - Abadi, M AU - Lamport, L PY - 1988/// UR - http://dx.doi.org/10.1109/LICS.1988.5115 ER -