High-integrity Java Applications using Circus

如今，计算机和计算机程序的使用已经很普遍了，但是每个计算机用户都知道程序会出错。当我们最喜欢的文本编辑器丢失了一点我们的工作时，这只是令人恼火，但当计算机程序（例如控制飞机部件的程序）出错时，后果可能会严重得多。软件确认和验证是开发这类应用程序的核心。事实上，软件行业通常在这些活动中花费了大量的资金。提高程序正确性所采取的措施之一是使用编程语言中可用的一组有限的特性。这通常意味着软件工程中大多数最新的进展都被忽略了。在这个项目中，我们建议提供开发、验证和验证设施，这些设施允许面向对象和现代实时计算模型用于安全关键系统的编程。特别地，我们将使用最流行的编程语言之一：Java，或者更具体地说，是由Open Group提出的用于高完整性工程的概要。作为我们的主要案例研究，我们将验证由Sun开发的第一个Java驱动的工业机器人的控制器部分。我们的一位合作者，Sun公司的一位高级工程师在一次采访中说，分布式实时系统真的很难构建，工程社区也不知道如何以一种连贯的、可重复的方式构建它们。（java.dzone.com/articles）实时Java正在进入工业自动化和汽车市场。律师们不允许Java机器人接近人类，即使是在JavaOne会议演示中。要在这样的市场中继续发展，需要更好的支持。编程只是现代系统开发的一个方面；通常，会产生大量额外的人工制品来指导和证明其设计。就像在砌砖和砂浆之前要制作几个大型建筑物的模型一样，在编写程序之前要开发和使用几个程序的规格和设计模型。这些模型有助于程序的确认和验证。让我们的土木工程比喻更进一步，我们观察到，就像一个建筑可以有不同的模型来反映不同的观点一样，比如电线、管道和平面图，我们也有一个系统的几个模型。不同的建模和设计符号专注于程序的不同方面：数据模型、并发和反应性行为、定时等等。没有任何一种符号或技术能够涵盖问题的所有方面，在开发大型复杂系统时需要使用它们的组合。在这个项目中，我们建议研究一种新的集成方法来验证和验证。我们的目标是提供一种可靠而实用的技术，涵盖数据建模、并发性、分布和定时。为此，我们计划研究已经在工业中成功应用的验证和验证技术的扩展和组合使用。我们不寻求符号和工具的特别组合，而是寻求一种合理的方法，为实际技术的使用提供可靠的基础。如果我们验证了机器人控制器的实质性部分，我们就成功了：使用用我们的符号编写的模型，我们将应用我们的技术来验证现有实现的部分，使用我们验证的安全关键Java实现来执行它。我们的工业合作伙伴将提供成功的衡量标准，以及我们的结果对他们的实践或商业计划的影响。

The use of computers and computer programs is pervasive nowadays, but every computer user knows that programs go wrong. While it is just annoying when our favourite text editor loses a bit of our work, the consequences are potentially much more serious when a computer program that, for instance, controls parts of an airplane goes wrong. Software validation and verification are central to the development of this sort of application. In fact, the software industry in general spends a very large amount of money in these activities. One of the measures taken to promote correctness of programs is the use of a restricted set of features available in programming languages. This usually means that most of the more recent advances in software engineering are left out. In this project, we propose to provide development, validation, and verification facilities that allow object-orientation and a modern real-time computational model to be used for the programming of safety-critical systems. In particular, we will work with one of the most popular programming languages: Java, or more specifically, its profiles for high-integrity engineering proposed by the Open Group. As our main case study, we will verify parts of the controller of the first Java Powered Industrial Robot, developed by Sun. One of our collaborators, a senior engineer in Sun tells in an interview that Distributed Real-Time Systems are really hard to build and the engineering community doesn't really know how to build them in a coherent repeatable way. (java.dzone.com/articles) Real-Time Java is entering the industrial automation and automotive markets. Lawyers did not allow the Java Robot to get anywhere near a human, even in a JavaOne conference demo. To proceed in that kind market, better support is needed.Programming is just one aspect of the development of a modern system; typically, a large number of extra artefacts are produced to guide and justify its design. Just like several models of a large building are produced before bricks and mortar are put together, several specification and design models of a program are developed and used before programs are written. These models assist in the validation and verification of the program. To take our civil engineering metaphor one step further, we observe that, just like there can be various models of a building that reflect several points of view, like electricity cabling, plumbing, and floor plans, for example, we also have several models of a system. Different modelling and design notations concentrate on different aspects of the program: data models, concurrent and reactive behaviour, timing, and so on. No single notation or technique covers all the aspects of the problem, and a combination of them needs to be employed in the development of large complex systems. In this project, we propose to investigate a novel integrated approach to validation and verification. Our aim is to provide a sound and practical technique that covers data modelling, concurrency, distribution, and timing. For that, we plan to investigate the extension and combined use of validation and verification techniques that have been successfully applied in industry. We do not seek an ad hoc combination of notations and tools, but a justified approach that provides a reliable foundation for the use of practical techniques. We will have succeeded if we verify a substantial part of the robot controller: using a model written in our notation, we will apply our techniques to verify parts of the existing implementation, execute it using our verified implementation of Safety-critical Java. Measure of success will be provided by our industrial partners and the influence of our results in their practice or business plans.