Detta dokument presenterar vårt arbete med att använda modelldriven teknik för att etablera en säkerhetssäkrad implementering av programvara för infusionspump med Patientkontrollerad analgesic (PCA) baserad på den generiska PCA-referensmodellen som tillhandahålls av USA:s Food and Drug Administration (FDA). Referensmodellen översattes först till ett nätverk av tidsinställda automata med hjälp av UPAAL-verktyget. Dess säkerhetsegenskaper säkerställdes sedan enligt den uppsättning allmänna säkerhetskrav som FDA också tillhandahöll. När referensmodellens säkerhet väl hade fastställts använde vi TIMES-verktyget för att automatiskt generera plattformsoberoende kod som ett preliminärt genomförande. Koden var sedan utrustad med hjälputrustning för gränssnitt med pumphårdvara och utplacerad på en riktig PCA-pump. Experiment visar att koden fungerade korrekt och effektivt med den riktiga pumpen. För att säkerställa att koden inte innebär någon överträdelse av säkerhetskraven utvecklade vi också en testbädd för att kontrollera överensstämmelsen mellan referensmodellen och koden genom överensstämmelseprovning. Utmaningar och lärdomar från vårt arbete diskuteras också i detta dokument.
I REF formaliserades en prototyp av den Generic Patient-Controlled Analgesic (GPCA) infusionspumpsregulatorn med hjälp av UPAAL-modellen, och sedan användes denna modell för att generera plattformsoberoende C-kod.
Safety-assured development of the GPCA infusion pump software
{'venue': "EMSOFT '11", 'journal': None, 'mag_field_of_study': ['Computer Science']}