The current paper gives an insight in the problem domain of formalization of software development, highlighting the potential advantages of usage of formal methods. The described research is strongly based on MDA, thus emphasizing the role of modelling process, as well as transformation of the models, in the modern software engineering. A number of inconsistensies originated from employment of the described methods during diverse stages of software development process are identified, providing the possible solutions and tracing the possible directions of the future research. A special attention is paid to the topic of formal specification of systems, using paradigms of category theory and topological modeling of functioning. In order to provide an adequate analysis and description of a problem domain, the sketch approach is discussed; its combination with the method of topological modelling of functioning is useful for modeling of the functional side of the system, as well as for mapping between the problem domain and the internal structue of a system. As one of the areas of application for formal methods the process of creation of embedded architectures is discussed.