zbMATH — the first resource for mathematics

Real-time Maude: A tool for simulating and analyzing real-time and hybrid systems. (English) Zbl 0962.68109
Futatsugi, Kokichi, The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18-20, 2000. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 36, 22 p., electronic only (2000).
Summary: Rewriting logic can be used to specify a wide range of real-time and hybrid systems under a variety of time models, including discrete and dense time models. The Real-Time Maude tool, built on top of the Maude rewriting logic language, supports specification of real-time and hybrid systems in timed modules and timed object-oriented modules, which are transformed into equivalent Maude modules. The tool then supports execution of such specifications in several rewrite modes, corresponding to different criteria for advancing time. Besides system simulation by default execution in a given rewrite mode, the tool has a library of execution strategies and commands that can search all the possible computations from an initial state, within given rewrite mode and search bounds, to partially model check desired properties, including properties expressible in a class of linear time timed temporal logic formulas. The paper discusses the tool’s theoretical basis, its specification language, and its library of evaluation and search strategies. The user can add new formal analysis strategies to the library, as illustrated by a scheduling case study. We also summarize our experience with applications and our future plans.
For the entire collection see [Zbl 0957.00046].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q42 Grammars and rewriting systems
Full Text: Link