SQLfast (SQL Formal AnalysiS Tool) is a bash script which takes an ASLan++ specification as input and, by using the ASLan++ translator, generates a transition system in the low-level language ASLan. It then calls the model- checker CL-AtSe and generates an Abstract Attack Trace (AAT) as an MSC if an attack was found. SQLfast automatically detects which type of SQLi has been exploited and, in an interactive way, generates the curlcurl or sqlmap commands to concretize the SQLi reported. This helps the modeler in the testing of the AAT over the concrete web application.
Details on how the approach works can be found here.