In previous work, constraint automata have been introduced as a uniform model for behavioral interfaces of components, (possibly dynamic) component connectors and systems consisting of several components and their glue code. The purpose of the paper is to provide an overview of the techniques for specifying and verifying temporal requirements, conditions on the data flow at the I/O-ports of components and alternating-time properties that have been designed for constraint automata. The paper presents the syntax and semantics of the logics, sketches the model checking algorithms, summarizes the main features of the implementation within the tool Vereofy and reports on experimental studies.