将 SCJ 任务规范精化为并行处理器设计

安全关键 Java（Safety-Critical Java, SCJ）是一项近期技术，它限制了 Java 的执行和内存模型，使得应用程序可以针对其实时属性和内存安全使用进行静态分析和认证。我们的兴趣在于开发全面且可靠的技术，用于采用构造正确（correct-by-construction）方法对 SCJ 程序进行形式化规范、精化、设计和实现。作为这项工作的一部分，我们在此介绍一系列具有通用性的定律和模式，用于将 SCJ 任务规范精化为 SCJ 编程范式中使用的并行处理器设计。我们的符号体系结合了 Circus 家族的语言，支持状态丰富的反应式模型，并增加了类对象和实时属性。我们的工作是为 SCJ 提炼编程定律的第一步，并契合我们先前开发的用于推导 SCJ 程序的精化策略。