Research Initiation Award: Cleopatra: A Programming Environment for Embedded Time-Critical Systems

可预测性--预测实现不会违反一组特定要求的能力--是嵌入式系统的一个至关重要的、非常理想的属性。本研究旨在开发用于构建可预测的时间关键型系统的编程环境(语言、库和工具)。该环境的主干是Cleopatra，这是一种编程语言，显然非常适合嵌入式系统的要求。Cleopatra采用类似C的命令式语法来描述计算，这使得它更容易合并到已经使用C的应用程序中。它是事件驱动的，因此适合嵌入式过程控制应用程序。它是面向对象的和组合的，因此提倡模块化和可重用性。Cleopatra在语义上是合理的；它的对象可以机械地和明确地转换为用于验证目的的形式TRA自动机，这可以使用模型检查或定理提供技术来实现。自1989年以来，克利奥帕特拉的祖先一直被用作嵌入式时间关键型机器人过程的规范和模拟语言。这项研究的目标更进一步。它的目标是建立一个基于克利奥帕特拉的综合支持环境，对学术界和工业界的实时系统开发人员都很有用。

Predictability - the ability to foretell that an implementation will not violate a set of specified requirements - is a crucial, highly desirable property of embedded systems. This research aims at developing a programming environment (language, libraries, and tools) for building predictable time-critical systems. The backbone of the environment is CLEOPATRA, a programming language that is demonstrably well-suited for the requirements of embedded systems. CLEOPATRA features a C- like imperative syntax for the description of computation, which makes it easier to incorporate in applications already using C. It is event-driven, and thus appropriate for embedded process control applications. It is object-oriented and compositional, thus advocating modularity and reusability. CLEOPATRA is semantically sound; its objects can be transformed, mechanically and unambiguously, into formal TRA automata for verification purposes, which can be pursued using model-checking or theorem providing techniques. Since 1989, an ancestor of CLEOPATRA has been in use as a specification and simulation language for embedded time-critical robotic processes. The goal of this research goes one step further. It aims at building an integrated CLEOPATRA-based support environment that would be useful for real-time system developers, both in academia and in industry.