Abstract :
In order to precisely analyze healthcare workflows, we examine how healthcare workflows can be modeled and verified with an elementary and concise timed CSP extension. To avoid considering healthcare workflows in isolation, we investigate the usage of our CSP dialect for formally modeling workflows alongside the instruction model of the openEHR specification set, which is a general, maintainable, and interoperable approach to electronic health records. Hence, we present a CSP model for openEHR instructions, which allows timed reasoning, and also integrates a basic notion of data and undefinedness. We show that this CSP dialect is suited to verify important properties of healthcare workflows, like workflow consistency, checking against timed specifications, and resource scheduling.
Keywords :
communicating sequential processes; formal specification; formal verification; health care; medical information systems; open systems; CSP dialect; electronic health record; formal model; healthcare workflow; instruction model; interoperable approach; maintainable approach; model checking; openEHR specification set; timed reasoning; Data models; Medical services; Real time systems; Semantics; Standards; Synchronization; CSP; Formal Methods; Healthcare Workflows; OpenEHR; Verification;
