Reactive systems developing by formal specification transformations

The design of reactive systems requires formal approaches in order to facilitate verification and validation at each step. Methods based on formal logic (automata, formal methods, etc.) have been suggested previously, but they often work only in a specific domain and are generally only possible with specialized users. In an attempt to overcome these restrictions, this paper proposes a global approach based on rewriting logic. It proposes a method for reactive systems analysis, specification and validation based on a reduction process. The target program generation is valid because it uses a formal transformation process. A grounding in theory is not a prerequisite for users. The method integrates modularity and abstraction and follows the main principles of an object-oriented approach