Reasoning about Implicit Invocation

8 years 9 months ago
Reasoning about Implicit Invocation
Implicit invocation SN92, GN91] has become an important architectural style for large-scale system design and evolution. This paper addresses the lack of speci cation and veri cation formalisms for such systems. Based on standard notions from process algebra and trace semantics, we de ne a formal computational model for implicit invocation. A veri cation methodology is presented that supports linear time temporal logic and compositional reasoning. First, the entire system is partioned into groups of components (methods) that behave independently. Then, local properties are proved for each of the groups. A precise description of the cause and the e ect of an event supports this step. Using local correctness, independence of groups, and properties of the delivery of events, we infer the desired property of the overall system. Two detailed examples illustrate the use of our framework.
David Garlan, Somesh Jha, David Notkin
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Authors David Garlan, Somesh Jha, David Notkin
Comments (0)