It is notoriously difficult to define, or even to understand, the behavior of a system of interacting asynchronous processes. Improbable sequences of events that lead to errors are easily overlooked by a protocol designer. If such errors occur in practice, they will be virtually irreproducible and very hard to fix. A distinct advantage of an automated validator is that it has no preconceived notions about what is meant or what is likely in a protocol definition: it examines possibilities not probabilities. It can patiently perform the analysis for millions of cases, faster and more accurately than could ever be done by hand. An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually. This type of validation is traditionally performed by the symbolic execution of a finite state machine model of the system studied. The author presents an overview of existing validation techniques and methods. The implementation of Aggregate specification safety and livenes is also presented: described safety and livenes properties, algorithms and implementation. Described experiments with system, and results compared with world-famous validation system SPIN. Performance of implemented algorithms evaluated. Given some suggestions for further development of automated aggregate specification validation system.