This tool paper presents Caos: a methodology and a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and interactive diagrams that animate and provide insights over the structure and the semantics of a given abstract model with operational rules. Caos follows an approach in which theoretical foundations and a practical tool are built together, as an alternative to foundations-first design ("tool justifies theory") or tool-first design ("foundations justify practice"). The advantage of Caos is that the tool-under-development can immediately be used to automatically run numerous and sizeable examples in order to identify subtle mistakes, unexpected outcomes, and unforeseen limitations in the foundations-under-development, as early as possible. We share two success stories of Caos' methodology and framework in our own teaching and research context, where we analyse a simple while-language and a choreographic language, including their operational rules and the concurrent composition of such rules. We further discuss how others can include Caos in their own analysis and Scala tools.

翻译：本文介绍Caos：一个面向形式模型结构化操作语义的计算机辅助设计方法论与编程框架。该框架包含一系列Scala库及工作流，可生成可视化交互式图表，对具有操作规则的给定抽象模型的结构与语义进行动态展示并提供深度洞察。Caos采取理论基础与实践工具协同构建的方案，区别于"基础先行设计"（即"工具验证理论"）或"工具先行设计"（即"基础佐证实践"）。Caos的优势在于：正在研发的工具可立即用于自动运行大规模多样化示例，从而尽早识别基础理论构建中的细微错误、意外结果及未预见的局限性。我们分享了Caos方法论与框架在自身教学与研究中的两个成功案例：分析了简单while语言与编排语言，涵盖其操作规则及规则的并发组合。最后探讨了其他研究者如何在自身分析与Scala工具中集成Caos。