Modeling and formal verification for software self-adaptation are the basis to improve development efficiency and to ensure reliability of self-adaptive software. However, there is a gap between visual modeling and formal modeling of software self-adaptation in existing work, which to some degree hampers the development of self-adaptive software. In order to systematically support modeling and formal verification for self-adaptive software, an approach called MV4SAS is proposed in this paper by incorporating the visual UML and the strictly defined timed automata. Firstly, the modeling facilities are defined by introducing new stereotypes, tagged values and constraints with UML extending mechanism, and the structural and behavioral models are created on the ground of the newly created facilities. Secondly, the behavioral model of self-adaptive software is mapped to timed automata network according to the predefined transformation algorithm, and the formal model of self-adaptive software is then created. Finally, using the model-checking tool UPPAAL, the reliability of software self-adaptation is verified with a set of predefined properties. Case study shows that the proposed approach can effectively reduce the modeling and verification complexity and improve development efficiency and reliability of self-adaptive software.