An Agile Formal Specification Language Design Based on K Framework

TL;DR

This paper presents an Agile Formal Specification Language (ASL) based on the K Framework and YAML, designed to simplify and accelerate formal specification writing for software verification.

Contribution

The paper introduces a novel agile formal specification language that integrates YAML and the K Framework, along with a translation algorithm for verification, improving efficiency and scalability.

Findings

Reduces code size for specifications

Enhances agility in formal specification writing

Enables scalable and efficient formal verification

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.