King, AndrewSokolsky, OlegLee, Insup2023-05-222023-05-222013-11-132014-01-06https://repository.upenn.edu/handle/20.500.14332/7960Modal specifications are classical formalisms that can be used to express the functional variability of systems; it is particularly useful for capturing the stepwise refinement of component-based design. However, the extension of such formalisms to real-time systems has not received adequate attention. In this paper, we propose a novel notion of time-parametric modal specifications to describe the timing as well as functional variability of real-time systems.We present a specification theory on modal refinement, property preservation and compositional reasoning. We also develop zone-graph based symbolic methods for the reachability analysis and modal refinement checking. We demonstrate the practical application of our proposed theory and algorithms via a case study of medical device cyber-physical systems.Computer EngineeringComputer SciencesReport