文章基本信息

标题：Toward a Dependability Case Language and Workflow for a Radiation Therapy System
本地全文：下载
作者：Michael D. Ernst ; Dan Grossman ; Jon Jacky 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：32
页码：103-112
DOI：10.4230/LIPIcs.SNAPL.2015.103
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We present a near-future research agenda for bringing a suite of modern programming-languages verification tools - specifically interactive theorem proving, solver-aided languages, and formally defined domain-specific languages - to the development of a specific safety-critical system, a radiotherapy medical device. We sketch how we believe recent programming-languages research advances can merge with existing best practices for safety-critical systems to increase system assurance and developer productivity. We motivate hypotheses central to our agenda: That we should start with a single specific system and that we need to integrate a variety of complementary verification and synthesis tools into system development.
关键词：Synthesis; Proof Assistants; Verification; Dependability Cases; Domain Specific Languages; Radiation Therapy