King, Andrew L.Sokolsky, OlegLee, InsupFeng, Lu2023-05-222023-05-222013-08-212013-08-29https://repository.upenn.edu/handle/20.500.14332/6826The on-demand approach, where systems are assembled from components by lay users, has seen success in the consumer electronics industry. Currently, there is growing demand for on-demand capabilities in medical systems so caregivers can create larger medical systems from smaller medical devices. Unlike consumer electronics, medical systems pose challenges for the on-demand approach due to attributes such as device complexity, device variability and safety requirements. In this paper, we propose a formal specification language for on-demand (medical) systems. Our approach is based on the formalism of Modal I/O Automata, which allows system designers to express complex device requirements and can be used to reason about safety and liveness properties of on-demand medical systems directly from their specifications. We illustrate the applicability of our approach through a case study of a closed-loop patient controlled analgesia system.The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-53956-5_14CPS MedicalComputer EngineeringComputer SciencesPresentation