Verification of ORM-based Controllers by Summary Inference
收藏资源简介：
The folder structure in icse2022-subm-data-1008-orm-verification-revised is as follows. ControllerVerificationData contains results corresponding to Section 5.2 of<br> the paper. The folder hierarchy within this is: benchmark name -> Controller class name -> "Alloy" -> a .als file (i.e., Alloy model/summary generated by our tool)<br> corresponding to each controller method, with assertions added<br> manually in all cases were they were expressible. "Output" -> outputs from Alloy for the assertions. multipage-data contains results corresponding to Section 5.3 of the paper. "properties" -> each .txt file contains a property (basically, a \psi as in Section<br> 3.1 in the paper), written by us, in Alloy form. (For "Unexpressed"<br> properties, we wrote a dummy property.) "toCheck" -> a property number -> Generated Alloy files for this property (one Alloy file for Property<br> (A) and one each for Property (I), see Section 3.1 in the paper) A .txt file for each Alloy file, containing Alloy checker's output. "summary.txt" contains a summary of all the information above Mutation-Analysis contains results corresponding to Section 5.5 of the<br> paper. Each leaf level folder under this contains: Alloy file generated for a mutated version of the benchmark, with<br> assertions added manually. The description of the mutation (in the .desc file) A .out file containing output from the Alloy checker for the assertions<br> in the .als file. JPF contains results corresponding to Section 5.6 of the paper. Each leaf-level folder contains results pertaining to one of the 16<br> assertions. The .java file contains a driver that initializes the tables,<br> calls the controller, and checks the assertion. The .jpf file is required<br> by JPF, and the .out file shows the JPF output. Sources are present in two folders:<br> -ControllerSummaryInference-src: Code for inferring relational-algebraic summaries of Spring-based web applications and alloy translation.<br> -multipage-src: Code for checking trace properties.<br> The file other-details.pdf contains syntax directed rules as well as loop patterns in tool which form the approach to infer relational summaries from ORM controllers.
