Safety-Critical Java Virtual Machine Services
Safety-Critical Java Virtual Machine Services
复制标题
DOI：
10.1145/2822304.2822307
复制
发表时间：
2015-10
期刊：
影响因子：
--
通讯作者：
James Baxter;Ana Cavalcanti;A. Wellings;Leo Freitas
中科院分区：
文献类型：
--
作者：
James Baxter;Ana Cavalcanti;A. Wellings;Leo Freitas
为了确保安全关键Java（SCJ）程序正确、安全地运行，它们运行的虚拟机必须显示为正确运行。然而，据我们所知，目前我们甚至没有对这种虚拟机的要求的明确规范。在本文中，我们提出了这些要求的SCJ API和基础设施的识别，根据SCJ标准的要求，并考虑到现有的虚拟机SCJ。形式化方法在建模和引出需求以及建立实现的正确性方面提供了一个强大的工具。我们还在这里提出了一个正式的模型的要求写在马戏团规范语言，这已经被用于验证SCJ程序的技术。我们的工作是一个贡献，建立一个框架，充分验证系统使用SCJ的发展。
To ensure that Safety-Critical Java (SCJ) programs run correctly and safely, the virtual machine they run on must be shown to operate correctly. To the best of our knowledge, however, currently we do not even have a clear specification of the requirements for such a virtual machine. In this paper, we present an identification of these requirements for the SCJ API and infrastructure, based on the requirements of the SCJ standard and on consideration of existing virtual machines for SCJ. Formal methods provide a powerful tool in modelling and eliciting requirements, and establishing correctness of implementations. We also present here a formal model of the requirements written in the Circus specification language, which has already been used in a technique for verification of SCJ programs. Our work is a contribution to establishing a framework for the development of fully verified systems using SCJ.