Building correct software systems is commonly accepted as both important and difficult. To achieve this, one has to address two basic issues: (i) offer suitable abstractions to formally specify specific classes of systems, (ii) allow the formal analysis of systems built using those abstractions. In this paper we review our results in this direction: we have proposed Object-Based Graph-Grammars (OBGGs) as a suitable set of abstractions to model concurrent, distributed, message passing and object-based based systems, coping with (i), and, coping with (ii), a set of transformations for OBGGs was proposed allowing one to employ several analysis methods, such as: model checking both functional and real-time properties, quantitative analysis using analytical methods, and verification through theorem proving.