forked from pvsioweb/pvsio-web
-
Notifications
You must be signed in to change notification settings - Fork 0
/
index-cover-page.html
138 lines (127 loc) · 10.5 KB
/
index-cover-page.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
<!DOCTYPE HTML>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>PVSio-Web Interactive Prototype Builder</title>
<link href="cover_page/css/bootstrap-theme.min.css" rel="stylesheet">
<link href="cover_page/css/bootstrap.min.css" rel="stylesheet" media="screen">
<link href="cover_page/css/coverpage-style.css" rel="stylesheet" media="screen">
<link rel="stylesheet" href="cover_page/css/pipe.css">
</head>
<body>
<a class="forkme" href="https://github.com/thehogfather/pvsio-web"><img style="position: absolute; top: 0; right: 0; border: 0;" src="https://camo.githubusercontent.com/652c5b9acfaddf3a9c326fa6bde407b87f7be0f4/68747470733a2f2f73332e616d617a6f6e6177732e636f6d2f6769746875622f726962626f6e732f666f726b6d655f72696768745f6f72616e67655f6666373630302e706e67" alt="Fork me on GitHub" data-canonical-src="https://s3.amazonaws.com/github/ribbons/forkme_right_orange_ff7600.png"></a>
<div id="coverpage">
<div id="nav">
<ul class="container">
<li class="active"><a href="index.html">Home</a></li>
<li><a href="http://www.pvsioweb.org/pvsioweb.html" target="_blank">Live Version</a></li>
<li><a href="https://github.com/thehogfather/pvsio-web" target="_blank">Downloads</a></li>
<li><a href="#publications">Publications</a></li>
<!-- <li><a href="#!apidocs">API docs</a></li>-->
</ul>
<div class="container tagline">
<span class="version">PVSio-web 2.0 </span><span>Easily create interactive prototypes based on formal specifications.</span>
</div>
</div>
<div class="container">
<div class="screenshots">
</div>
</div>
<div id="intro">
<div class="container center-block">
<!-- <h3>About</h3>-->
<p>PVSio-web is a graphical environment that transforms the animation capabilities of the standard PVS theorem proving system with a sophisticated graphical front-end allowing interactive (human-computer) systems modelling and prototyping. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analysing commercial medical devices, and has been used to create training material for device developers and device users. For safety-critical medical device design, PVSio-web has been used with formal methods experts and with non-technical end users, including doctors and nurses.</p>
</div>
</div>
<div class="container run">
<p>
<a class="btn btn-lg btn-outline-inverse run" href="http://www.pvsioweb.org/pvsioweb.html" target="_blank" alt="Start PVSio-web">Run PVSio-web from our Web Server</a>
<a class="btn btn-lg btn-outline-inverse download" href="https://github.com/thehogfather/pvsio-web" target="_blank" alt="Start PVSio-web">Download PVSio-web</a>
</p>
</div>
<div id="content-wrap">
<div class="container center-block featured-videos" >
<h3>Featured videos</h3>
<div class="row">
<div class="col-md-6">
<a href="http://youtu.be/T0QmUe0bwL8?t=1m8s"><img src="cover_page/images/youtube-thumb.png" width="100%"></a>
</div>
<div class="col-md-6">
<h4>Design issues in medical user interfaces.</h4>
<p>
<a href="http://www.eecs.qmul.ac.uk/~masci/" target="_blank">Paolo Masci</a>, Queen Mary University of London, has used PVSio-web to create this video for hospitals, device manufacturers, and regulators to raise awareness about general user interface software issues.
</p>
</div>
</div>
</div>
</div>
<div id="content-wrap">
<div class="container center-block featured-videos" >
<h3>Featured demos</h3>
<div class="row">
<div class="col-md-6">
<a href="http://www.pvsioweb.org/demos/Radical7" target="_blank">
<h4>Radical7 patient monitor prototype.</h4>
<img src="cover_page/images/Radical7.png" width="200px"></a>
</div>
</div>
<hr/>
<div class="row">
<div class="col-md-6">
<a href="http://www.pvsioweb.org/demos/AlarisGP" target="_blank">
<h4>AlarisGP infusion pump prototype.</h4>
<img src="cover_page/images/AlarisGP.jpg" width="150px"></a>
</div>
</div>
</div>
</div>
<div id="publications">
<div class="container center-block">
<h3>Publications</h3><br/>
<h4>Tool papers</h4>
<ol>
<li>
<span class="title">``PVSio-web 2.0: Joining PVS to HCI.''</span> <span class="authors">P. Masci, P. Oladimeji, Y. Zhang, P. Jones, P. Curzon, H. Thimbleby. </span> <span class="inproc">Proceedings of 27th International Conference on Computer Aided Verification (CAV2015).</span> <span class="place">California, USA, 2015.</span> <a target="_blank" href="http://www.chi-med.ac.uk/research/downloadandcount.php?PPnum=PP310">[PDF]</a>
</li>
<li>
<span class="title">``PVSio-web: a tool for rapid prototyping device user interfaces in PVS.''</span><span class="authors">Patrick Oladimeji, Paolo Masci, Paul Curzon and Harold Thimbleby</span><span class="inproc">Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013). </span><span class="place">London, UK, 2013</span> <a target="_blank" href="http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP112">[PDF]</a>
</li>
</ol><br/>
<h4>Applications</h4>
<ol start="3">
<li>
<span class="title">``The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps.''</span> <span class="authors">
P. Masci, R. Rukšėnas, P. Oladimeji, A. Cauchi, A. Gimblett, Y. Li, P. Curzon, H. Thimbleby. </span> <span class="inproc">In Innovations in Systems and Software Engineering, Vol 11(2), Springer-Verlag. </span> <span class="place"> London, 2015 </span> <a target="_blank" href="http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP135" class="pdf">[PDF]</a>
</li>
<li>
<span class="title">``Formal Verification of Medical Device User Interfaces Using PVS.''</span> <span class="authors">P. Masci, Y. Zhang, P. Jones, P. Curzon, H. Thimbleby. </span> <span class="inproc">In ETAPS/FASE2014, 17th International Conference on Fundamental Approaches to Software Engineering, </span> <span class="place">Grenoble, France, 2014</span> <a target="_blank" href="http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP193" class="pdf">[PDF]</a>
</li>
<li>
<span class="title">``Tool demo: Using PVSio-web to demonstrate software issues in medical user interfaces.''</span> <span class="authors">P. Masci, P. Oladimeji, P. Curzon and H. Thimbleby. </span><span class="inproc">In 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014). </span><span class="place">Washington DC, USA, 2014</span> <a target="_blank" class="pdf" href="http://www.chi-med.ac.uk/research/bibdetail.php?PPnum=PP234">[PDF]</a>
</li>
<li>
<span class="title">``Combining PVSio with Stateflow.''</span> <span class="authors">P. Masci, Y. Zhang, P. Jones, P. Oladimeji, E. D’Urso, C. Bernardeschi, P. Curzon and H. Thimbleby. </span><span class="inproc">In 6th NASA Formal Methods Symposium (NFM2014). </span><span class="place">Houston, TX, 2014</span> <a class="pdf" href="http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP204" target="_blank">[PDF]</a>
</li>
<li>
<span class="title">``Model-based development of the Generic PCA infusion pump user interface prototype in PVS.''</span> <span class="authors">P. Masci, A. Ayoub, P. Curzon, I. Lee, O. Sokolsky, H. Thimbleby.</span> <span class="inproc">In Safecomp2013, 32nd International Conference on Computer Safety, Reliability and Security. </span> <span class="place">Toulouse, France 2013 </span><a target="_blank" class="pdf" href="http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP120">[PDF]</a>
</li>
<li>
<span class="title">``Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example.''</span> <span class="authors">P. Masci, A. Ayoub, P. Curzon, M.D. Harrison, I. Lee, H. Thimbleby. </span> <span class="inproc">
In EICS2013, 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, </span> <span class="place"> London, UK, 2013 </span> <a href="http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP114" class="pdf" target="_blank">[PDF]</a>
</li>
<li>
<span class="title">``On formalising interactive number entry on infusion pumps.''</span> <span class="authors"> P. Masci, R. Rukšėnas, P. Oladimeji, A. Cauchi, A. Gimblett, Y. Li, P. Curzon, H. Thimbleby. </span> <span class="inproc">
In FMIS2011, the 4th Intl. Workshop on Formal Methods for Interactive Systems. </span> <span class="place"> Limerick, Ireland, 2011 </span> <a target="_blank" href="http://www.chi-med.ac.uk/researchers/downloadandcount.php?PPnum=PP021" class="pdf">[PDF]</a>
</li>
</ol>
</div>
</div>
<div id="footer">
<div class="container center-block">
<p>Licenced under <a href="http://www.gnu.org/licenses/gpl-3.0.html">GPLv3</a>.</p>
<p>Would you like to collaborate? Contact <a href="mailto:[email protected]">Paolo Masci</a> or <a href="mailto:[email protected]">Patrick Oladimeji</a>.</p>
</div>
</div>
</div>
</body>
</html>