<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Paolo Masci</style></author><author><style face="normal" font="default" size="100%">Anaheed Ayoub</style></author><author><style face="normal" font="default" size="100%">Paul Curzon</style></author><author><style face="normal" font="default" size="100%">Insup Lee</style></author><author><style face="normal" font="default" size="100%">Sokolsky, Oleg</style></author><author><style face="normal" font="default" size="100%">Harold Thimbleby</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS</style></title><secondary-title><style face="normal" font="default" size="100%">Computer Safety, Reliability, and Security</style></secondary-title><tertiary-title><style face="normal" font="default" size="100%">Lecture Notes in Computer Science</style></tertiary-title></titles><keywords><keyword><style  face="normal" font="default" size="100%">formal methods</style></keyword><keyword><style  face="normal" font="default" size="100%">Medical devices</style></keyword><keyword><style  face="normal" font="default" size="100%">Model-based development</style></keyword><keyword><style  face="normal" font="default" size="100%">User interface prototyping</style></keyword></keywords><dates><year><style  face="normal" font="default" size="100%">2013</style></year></dates><urls><web-urls><url><style face="normal" font="default" size="100%">http://dx.doi.org/10.1007/978-3-642-40793-2_21</style></url></web-urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/masci/files/gpcaui-safecomp2013.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Springer Berlin Heidelberg</style></publisher><volume><style face="normal" font="default" size="100%">8153</style></volume><pages><style face="normal" font="default" size="100%">228-240</style></pages><isbn><style face="normal" font="default" size="100%">978-3-642-40792-5</style></isbn><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;A realistic user interface is rigorously developed for the US Food and Drug Administration (FDA) Generic Patient Controlled Analgesia (GPCA) pump prototype. The GPCA pump prototype is intended as a realistic workbench for trialling development methods and techniques for improving the safety of such devices. A model-based approach based on the use of formal methods is illustrated and implemented within the Prototype Verification System (PVS) verification system. The user interface behaviour is formally specified as an executable PVS model. The specification is verified with the PVS theorem prover against relevant safety requirements provided by the FDA for the GPCA pump. The same specification is automatically translated into executable code through the PVS code generator, and hence a high fidelity prototype is then developed that incorporates the generated executable code.&lt;/p&gt;
</style></abstract></record></records></xml>