Tools to enable Runtime Verification from HPL properties
Project description
HPL Runtime Verification
This project provides tools from which you can build and manage runtime monitors based on HPL properties.
Installation
Install this package with
pip install hpl-rv
Usage
Code Generation
This package provides a command line interface from which you can generate runtime monitors with a simple command.
# generating monitors from a specification file
hpl-rv gen -f my_spec.hpl
# generating monitors directly from properties
hpl-rv gen "globally: no /a"
# redirecting the output to a file
hpl-rv gen -o ./code.py "globally: some /b within 100ms"
When used as a library, you can generate Python code for a runtime monitor class with a few simple steps. For example:
from hplrv.gen import lib_from_properties
hpl_properties = ['globally: no (/a or /b)']
code: str = lib_from_properties(hpl_properties)
print(code)
Monitoring Dashboard
This package also includes a web-based dashboard that enables live feedback from runtime monitors in a human-friendly format.
To execute the web server for this dashboard, run the gui
command:
hpl-rv gui --host "127.0.0.1" --port 8080
Then, open the dashboard client with a web browser (e.g., on http://localhost:8080
).
Through the dashboard, you can connect to runtime monitors to get live feedback. To enable this feature, though, your runtime monitors should first start the feedback server.
For example, for code generated with lib_from_properties()
, the main script where these monitors are included should follow roughly the following guidelines.
from threading import Thread
from .generated_monitors import HplMonitorManager
man = HplMonitorManager()
man.live_server.host = '127.0.0.1'
man.live_server.port = 4242
thread: Thread = man.live_server.start_thread()
now: float = 0.0
man.launch(now)
try:
# sleep or feed messages to the monitors; example:
while True:
sleep(1.0)
now += 1.0
man.on_timer(now)
except KeyboardInterrupt:
pass
man.shutdown(now)
thread.join(10.0)
The call to live_server.start_thread()
is what enables the dashboard to get live feedback.
GitHub Features
The .github
directory comes with a number of files to configure certain GitHub features.
- Various Issue templates can be found under
ISSUE_TEMPLATE
. - A Pull Request template can be found at
PULL_REQUEST_TEMPLATE.md
. - Automatically mark issues as stale after a period of inactivity. The configuration file can be found at
.stale.yml
. - Keep package dependencies up to date with Dependabot. The configuration file can be found at
dependabot.yml
. - Keep Release Drafts automatically up to date with Pull Requests, using the Release Drafter GitHub Action. The configuration file can be found at
release-drafter.yml
and the workflow atworkflows/release-drafter.yml
. - Automatic package building and publishing when pushing a new version tag to
main
. The workflow can be found atworkflows/publish-package.yml
.
Tooling
This package sets up various tox
environments for static checks, testing, building and publishing.
It is also configured with pre-commit
hooks to perform static checks and automatic formatting.
If you do not use tox
, you can build the package with build
and install a development version with pip
.
Assume cd
into the repository's root.
To install the pre-commit
hooks:
pre-commit install
To run type checking:
tox -e typecheck
To run linting tools:
tox -e lint
To run automatic formatting:
tox -e format
To run tests:
tox
To build the package:
tox -e build
To build the package (with build
):
python -m build
To clean the previous build files:
tox -e clean
To test package publication (publish to Test PyPI):
tox -e publish
To publish the package to PyPI:
tox -e publish -- --repository pypi
To install an editable version:
pip install -e .
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.