Formal Methods (FMs) are currently essential for verifying the safety and reliability of software systems. However, the specification writing in formal methods tends to be complex and challenging to learn, requiring familiarity with various intricate formal specification languages and verification technologies. In response to the increasing complexity of software frameworks, existing specification writing methods fall short in meeting agility requirements. To address this, this paper introduces an Agile Formal Specification Language (ASL). The ASL is defined based on the K Framework and YAML Ain't Markup Language (YAML). The design of ASL incorporates agile design principles, making the writing of formal specifications simpler, more efficient, and scalable. Additionally, a specification translation algorithm is developed, capable of converting ASL into K formal specification language that can be executed for verification. Experimental evaluations demonstrate that the proposed method significantly reduces the code size needed for specification writing, enhancing agility in formal specification writing.

翻译：形式化方法当前对于验证软件系统的安全性和可靠性至关重要。然而，形式化方法中的规约编写往往复杂且难以学习，需要熟悉各种复杂的形式规约语言和验证技术。针对软件框架日益增加的复杂性，现有的规约编写方法无法满足敏捷性需求。为解决此问题，本文提出了一种敏捷形式规约语言（ASL）。ASL基于K框架和YAML非标记语言（YAML）定义。ASL的设计融入了敏捷设计原则，使形式规约的编写更简单、高效且可扩展。此外，我们开发了一种规约翻译算法，能够将ASL转换为可执行验证的K形式规约语言。实验评估表明，所提方法显著减少了规约编写所需的代码量，增强了形式规约编写的敏捷性。