Model Model Checking Checking Publish Subscribe Publish Subscribe Software Software Architectures Architectures David Garlan Carnegie Mellon University Research Approach Specification and analysis of software architectures Components and their interactions Architectural styles e g client server pipe filter publish subscribe Architectural frameworks e g for specific domains and product lines Why Architectural design is a critical design artifact Can explore system properties before implementation A good level of abstraction for reasoning about system properties especially quality attributes State of arch practice is informal needs formalism Amortized effort when architecture used by many systems Carnegie Mellon The Rare Glitch Project 2 David Garlan Specific Thrusts Past research Specification languages for software architecture Analysis of specific architectural frameworks Wright based on CSP High level architecture for distributed simulation Enterprise JavaBeans JavaPhone Tools for software architects Current research Specification and analysis of publish subscribe software architectures today s talk Compositional mechanisms for component interactions Self configuring systems Carnegie Mellon The Rare Glitch Project 3 David Garlan Publish Subscribe Architectures An architectural style components objects processes functions connectors event registration computational model event announcement triggers invocation of the zero or more methods tasks that are registered for that event Features Anonymous multi cast supports decoupling between components Widely used Hence easy to modify and maintain UIs Prog envts JavaBeans Visual Basic JINI CORBA robots Many variants synch asynch dispatch policies concurrency shared state Carnegie Mellon The Rare Glitch Project 4 David Garlan Examples Set Counter Set S has operations insert delete Counter C has operations inc dec Establish invariant S C Set Counter Distributed Simulation HLA Arbitrary number of simulations publish values of objects that they simulate Run time infrastructure RTI maintains state e g ownership of objects mediates protocols of interaction Many invariants e g each object is owned by a single simulation RTI Sim1 Carnegie Mellon The Rare Glitch Project 5 Simn David Garlan More Examples State based State based duals duals Shared variable triggered systems Sensor Actuator Variables Aka continuous query systems State changes trigger computations Comp1 Components read write shared variables but are otherwise independent Comp2 Real time periodic tasks Tasks placed in periodically scheduled buckets Tasks consume values of certain variables produce values of other variables Shared Variables Tasks within bucket must complete before bucket period Task1 1 Taskn 1 Task1 2 Taskn 2 Taskn 3 Carnegie Mellon The Rare Glitch Project 6 David Garlan Pub Sub Systems are Hard to Reason About Burden of correctness falls to system integrator Lots of inherent non determinism Order of invocation of multiple event recipients In transit events Non determinism in dispatch mechanism Questions that are hard to answer What do we want to say about such systems What s an invariant Do the components announce the events that they should announce What will be the effect of announcing a particular event Are there the correct event subscriptions If a new component is added will it break what is already there Carnegie Mellon The Rare Glitch Project 7 David Garlan Technical Approach Foundations Key ideas Events have semantics Explicit specification of non interference conditions Compositionality via component environment specn Rely guarantee verification framework Joint work with Juergen Dingel Somesh Jha Din98b Based on Jones rely guarantee approach Results It works but is hard to use and often requires stronger invariants than are necessary Temporal logic verification framework Explicit modeling of dispatcher Din98a Properties expressed in LTL Results Properties are more naturally expressed Carnegie Mellon The Rare Glitch Project 8 David Garlan Technical Approach Tools Features Based on LTL foundations mentioned earlier Specifications translated to Cadence SMV Model Checker input Attempts to reduce cost of a building a system model and b specifying the properties to check Provides a Parameterized Model Generator Supports certain Built in Checks Currently in early stages of development and experimentation Carnegie Mellon The Rare Glitch Project 9 David Garlan Parameterized Model Generator Generate most of the run time event delivery and dispatch mechanisms Greatly reduce cost of constructing model for pub sub systems Support common dispatcher alternatives Allow easy exploration of alternatives Delivery options Concurrency options Asynchronous immediate return from announcement Synchronous return after event completely processed Single thread per component Multiple threads per component Dispatch order FCFS Prioritized Lossy etc Carnegie Mellon The Rare Glitch Project 10 David Garlan Model Architecture Environment external event source Delivery Policy Dispatcher Event Announcement Data Exchange Interface Comp 1 Interface Event Delivery Comp N Shared state Carnegie Mellon The Rare Glitch Project 11 David Garlan Shared Environment external event source Delivery Policy Dispatcher Event Announcement Data Exchange Interface Comp 1 Interface Event Delivery Comp N Shared state Carnegie Mellon The Rare Glitch Project 12 David Garlan Built in Checks Provide many of the common sanity checks Move towards push button tools Special cases Model view topology UI event model Idempotent systems Procedure call pairs General consistency completeness checks Components respect event semantics Events that are published but not subscribed to Events that are subscribed to but not published Liveness properties Race conditions Carnegie Mellon The Rare Glitch Project 13 David Garlan Next Steps and and opportunities opportunities for for collaboration collaboration Tool development More built in checks parameterization options Alternative model checker substrates Bridge Applications Realistic problems C1 C2 D1 D2 Pub sub bridges Current plan is to work on part of NASA remote agent architecture Better linkage to code Auto generation of component models Counterexample explanation New specification capabilities Dynamism timing real time Carnegie Mellon The Rare Glitch Project 14 David Garlan More information ABLE Project web site www cs cmu edu able Papers All98 Formal Modeling and Analysis of