Runtime monitoring is an essential part of guaranteeing the safety of cyber-physical systems. Recently, runtime monitoring frameworks based on formal specification languages gained momentum. These languages provide valuable abstractions for specifying the behavior of a system. Yet, writing specifications remains challenging as, among other things, the specifier has to keep track of the timing behavior of streams. This paper presents the RTLola Playground, a browser-based development environment for the stream-based runtime monitoring framework RTLola. It features new methods to explore the static analysis results of RTLola, leveraging the advantages of such a formal language to support the developer in writing and understanding specifications. Specifications are executed locally in the browser, plotting the resulting stream values, allowing for intuitive testing. Step-wise execution based on user-provided system traces enables the debugging of identified errors.
翻译:运行时监控是确保信息物理系统安全的重要组成部分。近年来,基于形式化规范语言的运行时监控框架势头渐起。这些语言为描述系统行为提供了有价值的抽象。然而,由于规约者需要同时追踪各流的时间行为等多方面因素,编写规范仍具挑战性。本文提出RTLola Playground,一个基于浏览器的流式运行时监控框架RTLola开发环境。该平台创新性地探索了RTLola静态分析结果的呈现方法,充分利用形式化语言的优势辅助开发者编写与理解规范。规范可在浏览器中本地执行并生成结果流值可视化图表,支持直观的测试。基于用户提供的系统轨迹的逐步执行机制,可实现对已识别错误的调试。