Logic-Based Formalization of System Requirements for Integrated Clinical Environments

The concepts of integrated clinical environments and smart intensive care units refer to complex technological infrastructures where health care relies on interoperating medical devices monitored and coordinated by software applications under human supervision. These complex socio-technical systems have stringent safety requirements that can be met with rigorous and precise development methods. This chapter presents an approach to the formalization of system requirements for integrated clinical environments, using the Prototype Verification System, a theorem-proving environment based on a higher-order logic language. The approach is illustrated by modeling safety-related requirements affecting various aspects of an integrated clinical environment, and in particular the communication network. A simple but realistic wireless communication protocol will be used as an example of computer-assisted verification.