The Role of Formal Methods in Modeling and Simulating Today's Distributed Software Systems

The growing complexity of today's distributed software systems has led to the need for more and more powerful formal methods, in order to help designers with modeling and specifying such systems. The complexity of today's distributed systems can be viewed from two standpoints: (i) complexity in formally representing such systems, and (ii) complexity of the interaction among the entities forming a distributed system. The former can be solved by finding formal languages featuring a sufficient semantic richness to cope with the complexity of representation of distributed systems. The latter leads to systems whose behavior is unpredictable due to a great intricacy in the interaction among system's components. These systems are also called complex systems: a big challenge to be won is to find principles and methodologies to be applied to the coordination among components of a complex system. 

Recently, a lot of efforts have been made to apply self-organization principles to the engineering of complex systems and lead to the emergence of desired behavior from the complex interaction of (distributed) components featuring very simple behaviors. Since engineering of such systems remains a difficult task to be managed, what has been emerging is the lack of tools helping software designers in the early design stage of the software engineering process. In particular, formal methods appear to be a useful tool to develop prototypes of software systems even in the early stages of the engineering process. A big challenge is to find a formal framework complete enough both to formally represent today's distributed software systems, and to help designers to successfully develop new distributed software systems by exploiting the theory of complex systems. In the effort of developing such a framework, we found Maude as a suitable programming language to cope with this challenge. Maude is a programming language based on rewriting logic that can be used to model and specify many kinds of distributed and concurrent systems by using transition rules. Moreover, specifying a software system by Maude leads to a program that can be viewed both as an executable prototype and a behavior specification of the software system itself. 

In the first two years of his PhD, Matteo Casadei has been trying to develop a Maude-based framework to help designers in the attempt to apply self-organization to the engineering of distributed software systems based on complex-system theory. So far, this has led to the development of a stochastic framework to make executable models of complex systems and study the application of self-organizing techniques to the engineering of such systems. Moreover, this framework has been tested on two case studies based on distributed tuple-space systems, that is, systems featuring a tuple-space-based coordination among the composing entities. The first case study, called Collective sort, is a problem where a set of background processes is in charge of moving tuples within a network of distributed tuple spaces until reaching a complete information clustering. To achieve this goal, a self-organizing strategy is applied. The second, called SwarmLinda, is an extension of the original Linda tuple-space framework where self-organization is applied in order to provide a tuple-distribution strategy on network of (distributed) tuple spaces. In both cases, we adopted our framework to study the application of self-organization in the engineering process of these systems.

Furthermore, in order to prove the capability of Maude to be used for specifying coordination languages, we developed an executable model of A&A ReSpecT, a coordination language based on the concept of reaction that can be used to specify the behavior of tuple spaces. Having an executable specification of this language can be really useful when one needs to develop complex coordination policies, since it makes it easy to test the validity of the policies by means of simulations. As future work, we are planning to follow two different directions. On one hand we are going to apply model-checking techniques to our Maude framework in order to formally verify the satisfaction of interesting properties on the modeled systems. On the other hand we are going to improve the framework and test its performance on new case studies.