Abstract: Reasoning about Implicit Invocation
Implicit invocation has become an
important architectural style for large-scale system design and
evolution. This paper addresses the lack of specification and
verification formalisms for such systems. Based on standard
notions from process algebra and trace semantics, we define a
formal computational model for implicit invocation.
A verification 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 effect 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.
Home