An Agile Formal Specification Language Design Based on K Framework

TL;DR

This work proposes an Agile Formal Specification Language (ASL) built on the $K$ Framework and YAML to address the complexity of writing formal specifications while preserving verifiability. ASL enables concise, readable specifications with reusable types, functions, and specifications, and provides a translation algorithm to generate executable $K$ specifications for verification. Empirical results show substantial reductions in specification size (average roughly $76\%$ fewer lines) compared with $K$-based specifications, and clearer structure than CBMC in several cases. The approach enhances agility in formal specification writing, enabling scalable verification across languages via the Imports mechanism, while future work aims to support direct solver-based verification and broader applicability. Overall, ASL offers a practical path to combine rigorous formal methods with agile software development practices.

Abstract

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.

Figures (5)

• Figure 1: Overall technical framework for this work.
• Figure 2: Composition rules of YAML nodes in an ASL file.
• Figure 3: Agile design concepts in ASL.
• Figure 4: Translation algorithm flow chart.
• Figure 5: Specification comparison for 3 kinds of specification languages.