Mining specifications

Citations Over TimeTop 1% of 2002 papers

Abstract

Program verification is a promising approach to improving program quality, because it can search all possible program executions for specific errors. However, the need to formally describe correct behavior or errors is a major barrier to the widespread adoption of program verification, since programmers historically have been reluctant to write formal specifications. Automating the process of formulating specifications would remove a barrier to program verification and enhance its practicality.This paper describes specification mining, a machine learning approach to discovering formal specifications of the protocols that code must obey when interacting with an application program interface or abstract data type. Starting from the assumption that a working program is well enough debugged to reveal strong hints of correct protocols, our tool infers a specification by observing program execution and concisely summarizing the frequent interaction patterns as state machines that capture both temporal and data dependences. These state machines can be examined by a programmer, to refine the specification and identify errors, and can be utilized by automatic verification tools, to find bugs.Our preliminary experience with the mining tool has been promising. We were able to learn specifications that not only captured the correct protocol, but also discovered serious bugs.

Related Papers

• → Analysis of the Formal Specification Application for Train Control Systems(2009)5 cited
• → Formal requirements specification in safety-critical railway signaling system(2009)6 cited
• The Analysis of Formal Methods for Applying to Vital S/W in Train Control Systems(2007)
• 열차제어시스템 바이탈 소프트웨어를 위한 정형기법 적용 방안 분석(2007)
• Z와 Statechart에 의한 열차제어시스템 바이탈 소프트웨어 개발 방법 분석(2008)