The paper presents a compositional program model of multi-application programs and sketches a framework for compositional specification and verification of temporal properties of such programs.