A migration of computations from local computers or corporate networks to the ``cloud'' has recently become a widespread trend in the development of information technology. This trend poses new challenges for both computer science in general and software engineering in particular. A modern software solution is now not merely a solution for an isolated computational unit, nor is it just a solution for a complex of computational units with shared memory. It is rather a distributed software solution. However, the developer of a distributed software solution is in a situation of greater uncertainty if compared with the developer of a local software solution. Hence, the risk of making a design error is ever-increasing for the latter. Thus, the efficiency challenge of verifying and validating a software solution is yet more significant for this kind of development. The difficulty of addressing this challenge is also caused by the fact that any instrumental code distorts the distributed software's behavior. Thus, the prospective way to meet the challenge is to create a toolkit for supporting both the traditional dynamic software analysis and the static (formal) one. To address the challenges posed by cloud computing, this paper introduces a novel approach that combines formal methods with simulation modeling. It presents and grounds a general mathematical model that can be used as the original point for implementing such a toolkit.