MEDL语言与DFA模拟：实现实时系统需求的有效验证

运行时验证中的MEDL语言和DFA模拟的问题探讨了一种在实时系统需求规格化中至关重要的技术，特别是针对复杂的时序约束和安全属性的表达。MEDL（Model-based Execution and Checking Language）是由MaC（Monitoring, Checking, and Guidance）框架提出的，这是一种用于规范基于线性时间逻辑（Linear Temporal Logic, LTL）的安全属性的语言。LTL是一种强大的逻辑框架，它允许对系统行为进行精确描述，包括未来事件的顺序、持续时间和频率。 原始的MEDL语言虽然具有表达性的优势，但在处理特定特性时遇到挑战，如精确描述事件的时间顺序和频率。为了解决这些问题，MEDL-RE（MEDL with Regular Expressions）被引入，它扩展了MEDL，增加了正则表达式的支持，使得表达时序依赖性和约束更为直观。这有助于设计者更好地指定系统的动态行为模式。 然而，当试图通过模拟确定有限自动机（DFA, Deterministic Finite Automaton）来监控正则表达式时，可能会产生效率问题。DFA模拟会涉及到并发路径的多路模拟，这可能导致运行时间呈指数级增长，这对于大规模实时系统来说是不可接受的。因此，研究者提出了一种改进的方法，通过生成依赖图来识别并处理并发事件，以避免过度的并发模拟。 他们通过增加原DFA的替代转换，替代了多路径模拟，这样可以在不牺牲效率的前提下处理并发事件。这种方法的目标是实现高效的并发处理，同时保持对系统行为的精确控制。这项工作得到了多个研究资助机构的支持，强调了在实时系统验证中的实际应用价值。 关键词：运行时验证、DFA模拟、DFA、MEDL、时序约束、并发事件、安全属性、LTL。总结来说，该研究关注的是如何通过扩展MEDL和优化DFA模拟策略来提升实时系统验证的性能和有效性，特别是在处理复杂时序逻辑和并发特性时。