Kavli Affiliate: Long Zhang
| First 5 Authors: Jianyu Zhang, Long Zhang, Yixuan Wu, Feng Yang,
| Summary:
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.
| Search Query: ArXiv Query: search_query=au:”Long Zhang”&id_list=&start=0&max_results=3