A formalization, in the HOL Light theorem prover, of the block-diagram representations used to model biomedical control systems - including their underlying differential equations and Laplace-transform-based transfer functions - so that properties such as the overall transfer function and subsystem stability can be established by machine-checked deductive reasoning rather than error-prone manual proofs or round-off-prone numerical tools. It is developed for analyzing the control of physical human-robot interaction (pHRI) applications.
This paper argues for using interactive (higher-order-logic) theorem proving, rather than manual proofs or numerical tools, to analyze the control systems of biomedical engineering applications, focu…