SIESTA stands for the Simple ImperativE SpecificaTion lAnguage, a minimalist specification language for expressing properties. It is built on top of Java, which is the programming language whose API properties we wanted to specify, and the language that lots of developers are familiar with. It includes the minimal number of features necessary to express various kinds of behavioral properties. We do not aim for generality.
This repository is organized according to the following structure:
- the
replication-packagefolder contains the dataset of properties from PropertyDB, the language specification document, the applied questionnaires, and students' responses; - the
prototypefolder contains the tool prototype for using the language. - the
samplefolder contains a sample project already configured with the tool, specifying a particular property from our sample (StringBuilder_ThreadSafe).
- Java 1.8
- Apache Commons Lang 3-3.1
Considering the sample project, given the requirements, you only need to execute two commands in the command line:
> ant ajmlc
> ant ajmlrac
If you wish to test a different scenario where the property is not violated, you can change the main.class property from the build.xml file in line 38 to stringbuilderexample.StringBuilderSingleThreadDemo.
@inproceedings{TMR+:ICST2021,
author = {Leopoldo Teixeira and Breno Miranda and Henrique Reb{\^{e}}lo and Marcelo d'Amorim},
booktitle = {14th {IEEE} International Conference on Software Testing, Verification and Validation, {ICST} 2021, Virtual Event, April 12-16, 2021},
title = {{Demystifying the Challenges of Formally Specifying API Properties for Runtime Verification}},
publisher = {{IEEE}},
year = {2021}
}