Skip to content

STAMINA - the STochastic Approximate Model-checker for INfinite-state Analysis. Implemeted for servers with a REST API.

Notifications You must be signed in to change notification settings

fluentverification/stamina-server

Repository files navigation

STAMINA for Servers

This repository contains code to allow STAMINA to be run via a REST API.

Why are we doing this?

FLUENT has recieved some grant funding to use towards some Azure servers. While IBioSym is already running on these servers, we are trying to make STAMINA/STORM able to run on these Azure servers. This is why we have dockerized it and are writing this wrapper program to read REST API calls and start STAMINA.

Self Hosting

Because this API is also open source, interested users can host their own versions of it, potentially without timeout limitations, and point the web frontend we have on https://staminachecker.org/run to their own servers (i.e., when the version we host is down). When a user changes the API URL to point to their server, it only changes for their browser, but is remembered by the website.

Overview

Each job is assigned a id, sometimes called a jid or uid for job ID or unique ID. These are stored in a hashed set and associated with an IP address. You can access the details of a job with its ID from any IP address (maybe should change this).

Jobs are pruned every so often and time out every few minutes.

Endpoints

  • /jobs:
    • POST: Creates a job, which is a run of STAMINA with a specific model and properties file. Accepts application/json and multipart/form-data, and returns application/json.
    • GET: Gets the list of all jobs. Currently just errors because I haven't figured out a good way to authenticate yet.
    • DELETE (not yet implemented): Deletes a job with a specific ID.
  • /myjobs:
    • GET: Gets a list of all jobs associated with the current IP address.
    • DELETE: Deletes all active jobs associated with the current IP Address.
  • /rename:
    • POST: Renames a job with a certain ID.
  • /about:
    • GET: Gets some information about STAMINA
  • /checkjob
    • POST: Gets just the log information about a Job, given its UID in HTTP POST.
  • /kill
    • POST: Kills, but does not delete, a job. Job logs can still be viewed after it is killed, but not after it is deleted.

HTTPS via nginx and uwsgi

(Not applicable for Azure)

Wherever this is deployed on the host machine, we will need to use certbot to create HTTPS certificates. I have been looking at this article and believe that we will be able to deploy using the methodology presented in this article. We will need to install and set up nginx on the machine

About

STAMINA - the STochastic Approximate Model-checker for INfinite-state Analysis. Implemeted for servers with a REST API.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published