Kim, BaekGyuFeng, LuPhan, Linh T. XSokolsky, OlegLee, Insup2023-05-222023-05-222015-03-012015-06-12https://repository.upenn.edu/handle/20.500.14332/6857In the model-based implementation methodology, the timed behavior of the software is typically modeled independently of the platform-specific timing semantics such as the delay due to scheduling or I/O handling. Although this approach helps to reduce the complexity of the model, it leads to timing gaps between the model and its implementation. This paper proposes a platform-specific timing verification framework that can be used to formally verify the timed behavior of an implementation that has been developed from a platform-independent model. We first describe a way to categorize the interactions among the software, a platform, and the environment in the form of implementation schemes. We then present an algorithm that systematically transforms a platform-independent model into a platform-specific model under a given implementation scheme. This transformation algorithm ensures that the timed behavior of the platform-specific model is close to that of the corresponding implementation. Our case study of an infusion pump system shows that the measured timing delay of the system is bounded by the formally verified bound of its platform-specific model.© 2015 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.CPS Model-Based Designformal specificationprogram verificationschedulingsoftware metricstimingI/O handlingformal verificationinfusion pump systemmodel complexitymodel-based implementation methodologyplatform-independent modelplatform-specific modelplatform-specific timing semanticsplatform-specific timing verification frameworkschedulingtiming delayAutomataComputational modelingDelaysSemanticsSoftwareSynchronizationComputer EngineeringComputer SciencesSoftware EngineeringTheory and AlgorithmsPresentation