形式化方法的一个切入点：事件描述与分析
An Entry Point for Formal Methods: Specification and Analysis of Event Logs
摘要：
形式化规约语言由于完备验证方法所面临的严重的可扩展性问题而长期处于停滞状态。可扩展性验证承诺使用正式的规范来自动化部分更可扩展的测试艺术，但尚未广泛应用于实际系统，并且由于在线监控仪器的成本和复杂性而经常动摇。在本文中，我们将讨论正在进行的工作，应用基于事件的规范系统的日志机制的火星科学实验室在喷气推进实验室的任务。通过专注于日志分析，我们利用“仪器”已经实现，并与航天器进行通信所需的。我们认为，这项工作既显示了一个实用的方法，使用正式的规格测试，并打开有趣的研究途径，包括一个具有挑战性的规格学习问题。
英文摘要：
Formal specification languages have long languished, due to the grave scalability problems faced by complete verification methods. Runtime verification promises to use formal specifications to automate part of the more scalable art of testing, but has not been widely applied to real systems, and often falters due to the cost and complexity of instrumentation for online monitoring. In this paper we discuss work in progress to apply an event-based specification system to the logging mechanism of the Mars Science Laboratory mission at JPL. By focusing on log analysis, we exploit the "instrumentation" already implemented and required for communicating with the spacecraft. We argue that this work both shows a practical method for using formal specifications in testing and opens interesting research avenues, including a challenging specification learning problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
