文章基本信息

标题：Automated theorem proving for the systematic analysis of an infusion pump
本地全文：下载
作者：Michael D. Harrison ; Paolo Masci ; Jose Creissac Campos 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2014
卷号：69
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：This paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems.