A formal approach to monitoring web pages as spatio-temporal traces.
Please remember that to run the tool:
- an internet connection is required
- when not in headless mode, a desktop environment must be available on the running machine.
Alternatively, to run in headless mode, change the browser to
CHROME_HEADLESS
insource.*.kts
files.
To launch WebMonitor, two files must be provided in src/main/resources
: source.XXX.kts
and spec.YYY.kts
.
Once the required source.XXX.kts
and spec.YYY.kts
files are created, run the following commands.
./gradlew run --args="XXX YYY"
Or just
./gradlew run --args="XXX"
if XXX = YYY
Note that the first time you run the tool, it will download the required dependencies, so it might take a while.
To use it as a maven package, just include the following line in your build.gradle.kts
:
implementation("com.enniovisco:webmonitor:v1.1.0")
Check on Maven Central for alternative build tools ( e.g. Maven).
Since Windows 11, the default terminal is PowerShell, so the previous command should run out of the box. If it doesn't,
and you are using the good old fashion CLI (Why are you doing it? You should reconsider your priorities...), you can
substitute ./gradlew
with gradlew.bat
and the rest should work the same way.
Some examples are available in src/main/resources/examples
.
In general though, few lines are needed to run the tool on a new website.
The spec file contains the key information about the browsing session that will be run. An example follows:
// source.XXX.kts
import com.enniovisco.*
// Browsing window size:
WebSource.screenWidth = 600 // px
WebSource.screenHeight = 600 // px
// OPTIONAL: Change the browser used for the evaluation.
WebSource.browser = Browser.CHROME // - default - only allowed values currently are CHROME and FIREFOX
// Browsing session duration, after which the browser is closed
WebSource.maxSessionDuration = 5_000 // ms
// OPTIONAL: sets a waiting time before starting recording the browser (so that initial loading errors can be skipped by the analysis)
WebSource.wait = 1_000 // ms
// Browser's address of the analyzed page
WebSource.targetUrl = "https://enniovisco.github.io/webmonitor/"
The spec file contains the key information about the browsing session that will be run. An example follows:
// spec.YYY.kts
import com.enniovisco.*
Spec.atoms(
select { "h1" } read "visibility" equals "visible",
)
Spec.record(
after { "click" }
)
// Helper formulae
val screen = Spec.screen
val isVisible = Spec.atoms[0]
val f1 = isVisible and screen
val f2 = f1 and (eventually(isVisible) implies not(isVisible)) // some random complex formula to show operators.
// Final monitored formula
Spec.formula = f2
Special thanks to Moonlight and Selenium Webdriver, and the supporting developers.