Engineering processes for safety-critical systems describe the steps and sequence that guide engineers from refining user requirements into executable code, as well as producing the artifacts, traces, and evidence that the resulting system is of high quality. Process compliance focuses on ensuring that the actual engineering work is followed as closely as possible to the described engineering processes. To this end, temporal constraints describe the ideal sequence of steps. Checking these process constraints, however, is still a daunting task that requires a lot of manual work and delivers feedback to engineers only late in the process. In this paper, we present an automated constraint checking approach that can incrementally check temporal constraints across inter-related engineering artifacts upon every artifact change thereby enabling timely feedback to engineers on process deviations. Temporal constraints are expressed in the Object Constraint Language (OCL) extended with operators from Linear Temporal Logic (LTL). We demonstrate the ability of our approach to support a wide range of higher level temporal patterns. We further show that for constraints in an industry-derived use case, the average evaluation time for a single constraint takes around 0.2 milliseconds.

翻译：安全关键系统的工程过程描述了从用户需求精炼为可执行代码的步骤与序列，同时生成证明最终系统高质量的制品、追溯及证据。过程合规性侧重于确保实际工程工作尽可能紧密地遵循所描述的工程过程。为此，时间约束规定了理想的步骤顺序。然而，检查这些过程约束仍是一项艰巨任务，需要大量人工工作，且仅能在过程后期向工程师提供反馈。本文提出一种自动化约束检查方法，该方法能在每次制品变更时增量检查跨关联工程制品的时间约束，从而及时向工程师反馈过程偏差。时间约束通过扩展了线性时序逻辑（LTL）算子的对象约束语言（OCL）表达。我们证明了该方法支持广泛高阶时间模式的能力，并进一步表明，在工业衍生用例中，单条约束的平均评估时间约为0.2毫秒。