Talk "Specification and Analysis in Real-Time Maude"

by Peter Ölveczky

Wed, 11 January 2017 at 05:00 pm in Binz (Rügen), Germany

Abstract: Real-Time Maude extends the rewriting logic language and tool Maude to support the executable formal specification and analysis of real-time systems. Real-Time Maude emphasizes expressiveness and modeling convenience over algorithmic decidability of key properties, and is particularly suitable to model distributed real-time systems in an object-oriented style. In this talk I briefly introduce Real-Time Maude and some of its applications. I also explain that the satisfaction of timed CTL (TCTL) formulas under the natural continuous semantics for (dense-time) timed Kripke structures can be reduced to a model-checking problem in the pointwise semantics for a large class of timed Kripke structures, which includes many discrete-event systems. This abstraction gives a sound and complete TCTL model checking procedure for time-robust real-time rewrite theories also for dense time domains. We have implemented such a TCTL model checker for Real-Time Maude. Our model checker provides for free a sound and complete TCTL model checker for subsets of modeling languages, such as Ptolemy II, AADL, and Timed Rebeca, which have Real-Time Maude analysis integrated into their tool environments.