Abstrakt. Tillförlitlighet hos medicintekniska produkter som CARA Infusion Pump Control System är av yttersta vikt med tanke på att dessa produkter används på patienter i kritiskt tillstånd. Infusionspumpens styrsystem omfattar inbyggda processorer och tillhörande inbäddad programvara för övervakning samt styrgivare och ställdon som gör det möjligt för inbäddade system att interagera med sina miljöer. Denna typ av infusionspumpkontrollsystem ökar komplexiteten i att säkerställa det totala systemets tillförlitlighet. De traditionella metoderna för att utveckla inbyggda system är otillräckliga för sådana säkerhetskritiska anordningar. I detta dokument studerar vi tillämpningen av formella metoder på kravfångning och analys av Infusion Pump Control System. Vår strategi består av två faser. Den första fasen är att omvandla de informella konstruktionskraven till en uppsättning referensspecifikationer med hjälp av ett formellt system, i detta fall EFSM (Extended Finite State Machines). Den andra fasen är att översätta referensspecifikationerna till de verktyg som stöder formell analys, såsom SCR och Hermes. Detta gör det möjligt för oss att dra slutsatser om referensspecifikationerna. Vårt forskningsmål är att utveckla ett ramverk och metodik för integrerad användning av formella metoder i utvecklingen av inbyggda medicinska system som kräver hög säkerhet och förtroende.
Alur m.fl. REF använde sig av Extended Finite State Machines (EFSM) för att formellt modellera CARA, och kontrollerade specifikationerna med hjälp av verktyg som stöder formell analys, såsom SCR och Hermes.
Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System
{'venue': 'International Journal on Software Tools for Technology Transfer', 'journal': 'International Journal on Software Tools for Technology Transfer', 'mag_field_of_study': ['Computer Science']}