Composition and verification of formal behaviors