Developing Components in Presence of Re-entrance. Mikhajlov, L., Sekerinski, E., & Laibinis, L. In Wing, J., Woodcock, J., & Davis, J., editors, FM'99 — Formal Methods, volume 1709, of Lecture Notes in Computer Science, pages 721–721, Toulouse, France, September, 1999. Springer-Verlag. doi abstract bibtex Independent development of components according to their specifications is complicated by the fact that a thread of control can exit and re-enter the same component. This kind of re-entrance may cause problems as the internal representation of a component can be observed in an inconsistent state. We argue that the ad-hoc reasoning used in establishing conformance of components to their specifications that intuitively appears to be correct does not account for the presence of re-entrance. Such reasoning leads to a conflict between assumptions that component developers make about the behavior of components in a system, resulting in the component re-entrance problem. We formulate the modular reasoning property that captures the process of independent component development and introduce two requirements that must be imposed to avoid the re-entrance problem. Then we define a customized theory of components, component systems, and component refinement which models the process of component development from specifications. Using this theory, we prove that the formulated requirements are sufficient to establish the modular reasoning property.
@inproceedings{MikhajlovSekerinskiLaibinis99ComponentsReentrance,
address = {Toulouse, France},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Developing {Components} in {Presence} of {Re}-entrance},
volume = {1709},
doi = {10.1007/3-540-48118-4_19},
abstract = {Independent development of components according to their specifications is complicated by the fact that a thread of control can exit and re-enter the same component. This kind of re-entrance may cause problems as the internal representation of a component can be observed in an inconsistent state. We argue that the ad-hoc reasoning used in establishing conformance of components to their specifications that intuitively appears to be correct does not account for the presence of re-entrance. Such reasoning leads to a conflict between assumptions that component developers make about the behavior of components in a system, resulting in the component re-entrance problem. We formulate the modular reasoning property that captures the process of independent component development and introduce two requirements that must be imposed to avoid the re-entrance problem. Then we define a customized theory of components, component systems, and component refinement which models the process of component development from specifications. Using this theory, we prove that the formulated requirements are sufficient to establish the modular reasoning property.},
booktitle = {{FM}'99 — {Formal} {Methods}},
publisher = {Springer-Verlag},
author = {Mikhajlov, Leonid and Sekerinski, Emil and Laibinis, Linas},
editor = {Wing, Jeanette and Woodcock, Jim and Davis, Jim},
month = sep,
year = {1999},
pages = {721--721},
}
Downloads: 0
{"_id":"oxJzzhSyvuvt3qPLi","bibbaseid":"mikhajlov-sekerinski-laibinis-developingcomponentsinpresenceofreentrance-1999","author_short":["Mikhajlov, L.","Sekerinski, E.","Laibinis, L."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Toulouse, France","series":"Lecture Notes in Computer Science","title":"Developing Components in Presence of Re-entrance","volume":"1709","doi":"10.1007/3-540-48118-4_19","abstract":"Independent development of components according to their specifications is complicated by the fact that a thread of control can exit and re-enter the same component. This kind of re-entrance may cause problems as the internal representation of a component can be observed in an inconsistent state. We argue that the ad-hoc reasoning used in establishing conformance of components to their specifications that intuitively appears to be correct does not account for the presence of re-entrance. Such reasoning leads to a conflict between assumptions that component developers make about the behavior of components in a system, resulting in the component re-entrance problem. We formulate the modular reasoning property that captures the process of independent component development and introduce two requirements that must be imposed to avoid the re-entrance problem. Then we define a customized theory of components, component systems, and component refinement which models the process of component development from specifications. Using this theory, we prove that the formulated requirements are sufficient to establish the modular reasoning property.","booktitle":"FM'99 — Formal Methods","publisher":"Springer-Verlag","author":[{"propositions":[],"lastnames":["Mikhajlov"],"firstnames":["Leonid"],"suffixes":[]},{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]},{"propositions":[],"lastnames":["Laibinis"],"firstnames":["Linas"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Wing"],"firstnames":["Jeanette"],"suffixes":[]},{"propositions":[],"lastnames":["Woodcock"],"firstnames":["Jim"],"suffixes":[]},{"propositions":[],"lastnames":["Davis"],"firstnames":["Jim"],"suffixes":[]}],"month":"September","year":"1999","pages":"721–721","bibtex":"@inproceedings{MikhajlovSekerinskiLaibinis99ComponentsReentrance,\n\taddress = {Toulouse, France},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Developing {Components} in {Presence} of {Re}-entrance},\n\tvolume = {1709},\n\tdoi = {10.1007/3-540-48118-4_19},\n\tabstract = {Independent development of components according to their specifications is complicated by the fact that a thread of control can exit and re-enter the same component. This kind of re-entrance may cause problems as the internal representation of a component can be observed in an inconsistent state. We argue that the ad-hoc reasoning used in establishing conformance of components to their specifications that intuitively appears to be correct does not account for the presence of re-entrance. Such reasoning leads to a conflict between assumptions that component developers make about the behavior of components in a system, resulting in the component re-entrance problem. We formulate the modular reasoning property that captures the process of independent component development and introduce two requirements that must be imposed to avoid the re-entrance problem. Then we define a customized theory of components, component systems, and component refinement which models the process of component development from specifications. Using this theory, we prove that the formulated requirements are sufficient to establish the modular reasoning property.},\n\tbooktitle = {{FM}'99 — {Formal} {Methods}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Mikhajlov, Leonid and Sekerinski, Emil and Laibinis, Linas},\n\teditor = {Wing, Jeanette and Woodcock, Jim and Davis, Jim},\n\tmonth = sep,\n\tyear = {1999},\n\tpages = {721--721},\n}\n\n","author_short":["Mikhajlov, L.","Sekerinski, E.","Laibinis, L."],"editor_short":["Wing, J.","Woodcock, J.","Davis, J."],"key":"MikhajlovSekerinskiLaibinis99ComponentsReentrance","id":"MikhajlovSekerinskiLaibinis99ComponentsReentrance","bibbaseid":"mikhajlov-sekerinski-laibinis-developingcomponentsinpresenceofreentrance-1999","role":"author","urls":{},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","dataSources":["HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"],"keywords":[],"search_terms":["developing","components","presence","entrance","mikhajlov","sekerinski","laibinis"],"title":"Developing Components in Presence of Re-entrance","year":1999}