Jee, EunkyoungLee, InsupSokolsky, Oleg2023-05-222023-05-222010-10-182010-11-15https://repository.upenn.edu/handle/20.500.14332/6536We discuss the construction of an assurance case for the pace-maker software. The software is developed following a model-based technique that combined formal modeling of the system, systematic code generation from the formal model, and measurement of timing behavior of the implementation. We show how the structure of the assurance case reflects our development approach.The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-16561-0_33CPS Model-Based Designassurance casepacemaker challengemodel-driven developmentreal-time softwarePresentation