In this paper we propose a language for conveniently defining a wide range of execution strategies for real-time rewrite theories, and provide Maude-strategy-implemented versions of most Real-Time Maude analysis methods, albeit with user-defined discrete and timed strategies. We also identify a new time sampling strategy that should provide both efficient and exhaustive analysis for many distributed real-time systems. We exemplify the use of our language and its analyses on a simple round trip time protocol, and compare the performance of standard Maude search with our strategy-implemented reachability analyses on the CASH scheduling algorithm benchmark.

翻译：本文提出了一种语言，用于便捷地定义实时重写理论中的多种执行策略，并提供了大多数实时Maude分析方法的Maude策略实现版本，尽管这些方法使用用户定义的离散和定时策略。我们还识别出一种新的时间采样策略，该策略应为许多分布式实时系统提供高效且详尽的分析。我们通过一个简单的往返时间协议示例，展示了该语言及其分析的使用方法，并在CASH调度算法基准上比较了标准Maude搜索与我们策略实现的可达性分析的性能。