A formal methods toolkit for model-based development of human-machine interfaces
PVSio-web is a new graphical tool to prototype and analyse user interface software. It provides the typical functionalities of an animation environment that allows designers to load and simulate realistic user interfaces. Underneath, it uses SRI's state-of-the-art theorem prover PVS for analysis, and the pvsio component as a basis for simulation.
Simulations created with PVSio-web can be watched in this youtube video https://www.youtube.com/watch?v=T0QmUe0bwL8
Realistic prototypes created using PVSio-web can be found at the following links:
The full PVSio-web tool with limited features is also available at http://www.pvsioweb.org (please note that the web server has limited processing power so its response time might not be optimal; also, note that the file system is read-only, so you will not be able to save new prototypes or compile new models using this live version).
To install PVSio-web, first you need to install PVS and NodeJS, and then clone the PVSio-web github repository. This can be done as follows.
PVS is required to run PVSio-web. The tool can be downloaded from http://pvs.csl.sri.com/download.shtml Installation instructions are on the aforementioned website.
Once PVS is installed, please add the following PVS executable files to your PATH: pvs, pvsio and proveit. A simple way to do this is to create symbolic links to those files, and place the symbolic links in /usr/bin. For instance, if PVS is installed in /opt/PVS/pvs, the following commands executed in a Terminal window create the required symbolic links:
sudo ln -s /opt/PVS/pvs /usr/bin/pvs sudo ln -s /opt/PVS/pvsio /usr/bin/pvsio sudo ln -s /opt/PVS/proveit /usr/bin/proveit
Please note that the ln command requires a full path.
NodeJS is required to run PVSio-web. Please download and install NodeJS from http://nodejs.org Installation instructions are on the aforementioned website.
Create a directory where you would like to install PVSio-web on your local computer. Open a Terminal window in the created directory, and use 'git' to clone the PVSio-web repository:
git clone https://github.com/thehogfather/pvsio-web.git cd pvsio-web npm install
PVSio-web is now installed on your local computer!
To run pvsio-web, a backend and a frontend need to be started.
To start the backend: open a Terminal window in the pvsio-web directory, and use the following command (and leave the Terminal window open):
To start the frontend: open a browser (Firefox 21 or greater, or Chrome), and type the following address in the address bar:
To update pvsio-web to the latest version, open a Terminal window, and execute the following command from the pvsio-web directory:
Realistic simulations created with PVSio-web can be watched in this youtube video:
All simulation examples demonstrated in the youtube video are included in the PVSio-web distribution in examples/projects. To open these examples, start pvsio-web and click the "Open Projects" button of the pvsio-web frontend and select one of the examples from the list.
This project has the following setup:
To obtain the latest development versions of pvsio-web, you can clone our alpha branch on the github repository.
To clone the alpha branch, create a new directory (for example, pvsioweb-alpha), open a Terminal window, and execute the following commands from the created directory:
git clone https://github.com/thehogfather/pvsio-web.git -b alpha cd pvsio-web npm install
To test the client, start the pvsio-web backend by running the following command in a Terminal window (and leave the Terminal window open): ./start.sh
and type the following address in a browser window:
To test the server, run the following command in a Terminal window
To uninstall, delete the pvsio-web folder from your computer.