Formal Methods Seminar:
DYNAMITE: A TOOL FOR THE VERIFICATION OF ALLOY MODELS BASED ON PVS
Mariano Moscato, Postdoctoral Research Scholar, NIA
September 26, 2014, 11:00 am, NASA Langley, Bldg 1220, Rm 110
Host: Cesar Munoz (NASA Langley)
Abstract:
Formal analysis of software models can be undertaken following two approaches: the lightweight and the heavyweight. The former offers languages with simple syntax and semantics, supported by automatic analysis tools. Nevertheless, the analysis they perform is usually partial. The latter provides full confidence analysis of models, but often requires interaction from highly trained users. Alloy is a good example of lightweight method. Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT-solvers. The translation requires user-provided bounds on the sizes of data domains.
The analysis is limited by the bounds, and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary. As the main work of my PhD thesis, we developed the tool called Dynamite. It is an extension of PVS that embeds a complete calculus for Alloy. PVS is a well-known heavyweight method. It provides a semi-automatic theorem prover for higher order logic. Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi-automatic verification through theorem proving. It also improves the theorem proving experience by using the Alloy Analyzer to provide automatic functionality intended to early error detection, proof refinement and witness generation for existentially quantified properties.