Abstract: 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. A formal computational model for implicit invocation is presented. We develop a verification framework for implicit invocation that is based on Jones' rely/guarantee reasoning for concurrent systems. The application of the framework is illustrated with several examples. The merits and limitations of the rely/guarantee paradigm in the context of implicit invocation systems are also discussed.

Abstract: An increasingly important trend in the engineering of complex systems is the design of component integration standards. Such standards define rules of interaction and shared communication infrastructure that permit composition of systems out of independently-developed parts. A problem with these standards is that it is often difficult to understand exactly what they require and provide, and to analyze them in order to understand their deeper properties. In this paper we use our experience in modeling the High Level Architecture (HLA) for Distributed Simulation to show how one can capture the structured protocol inherent in an integration standard as a formal architectural model that can be analyzed to detect anomalies, race conditions, and deadlocks.

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

Abstract: A software architecture should expose important system properties for consideration and analysis. Performance-related properties are frequently of interest in determining the acceptability of a given software design. In this paper we show how queueing network modeling can be adapted to support performance analysis of software architectures. We also describe a tool for transforming a software architecture in a particular style into a queueing network and analyzing its performance.

Abstract: A critical issue for complex component-based systems design is the modeling and analysis of architecture. One of the complicating factors in developing architectural models is accounting for systems whose architecture changes dynamically (during run time). This is because dynamic changes to architectural structure may interact in subtle ways with on-going computations of the system.

In this paper we argue that it is possible and valuable to provide a modeling approach that accounts for the interactions between architectural reconfiguration and non-reconfiguration system functionality, while maintaining a separation of concerns between these two aspects of a system. The key to the approach is to use a uniform notation and semantic base for both reconfiguration and steady-state behavior, while at the same time providing syntactic separation between the two. As we will show, this permits us to view the architecture in terms of a set of possible architectural snapshots, each with its own steady-state behavior. Transitions between these snapshots are accounted for by special reconfiguration-triggering events.

Abstract: A critical issue for architectural design is the nature of the glue, or connectors, with which a system's parts are combined. Thus an important first step toward improving our ability to compose parts is to make to make connectors explicit semantic enties, where they can be documented, analyzed, and (sometimes) used to generate code. A number of notations for software architecture do precisely this. However, a key second step is to understand operations over connectors. In principle, such operations would permit one to produce new connectors out of old ones, adapt existing connectors to new contexts of use, and factor out common properties of connectors so they can be reused. In this paper we argue that the use of ``higher order connectors'' is one way to achieve this goal.