A formal approach to the specification and the behavior validation of real-time systems based on rewriting logic

Design of real time and concurrent systems requires formal approaches in order to facilitate verification and validation at each step. Methods based on formal logic have been previously suggested but they often work only in a specific domain and are generally only possible with specialized users. In an attempt to overcome these two restrictions, this paper proposes a method based on rewriting logic. 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. Different tools are available: a graphical editor for the specification of the structure and the behavior of the objects, an inference engine for rule validation and a generator of prototypes.