Abstract
A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle if a component need behave correctly only when its environment does, since each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.
Cite
CITATION STYLE
Abadi, M., & Lamport, L. (1990). Composing specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 430 LNCS, pp. 1–41). Springer Verlag. https://doi.org/10.1007/3-540-52559-9_59
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
