发表机构
Inria; Université Côte d'Azur（法国国家信息与自动化研究所; 蔚蓝海岸大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出基于CCSL的细化时序规范框架，分三层次引入时序知识，将随机信息作为细化附加，支持增量集成，并在OCaml工具及软件定义车辆用例中验证。
AI 中文摘要
实时系统和信息物理系统通过从抽象需求到平台部署的逐步细化过程进行开发。虽然时序知识在整个过程中不断演变，但现有的随机实时形式化方法通常要求从一开始就嵌入不确定性，或在获得新的时序信息时需要重建模型，这阻碍了迭代式时序工程。本文提出了一个基于时钟约束规范语言（CCSL）的面向细化的时序规范框架。该框架支持在三个层次上逐步引入时序知识：逻辑时序关系、定量实时约束和随机时序模型。随机信息不改变行为语义，而是作为细化直接附加到时序量上。这使得实现测量和操作观测能够在统一的声明性框架内增量式地纳入。我们在一个基于OCaml的仿真工具中实现了我们的方法，并在一个简化但具有代表性的软件定义车辆用例上进行了评估。
英文摘要
Real-time and cyber-physical systems are developed through successive refinements from abstract requirements to platform deployments. While timing knowledge evolves throughout this process, existing stochastic real-time formalisms typically require uncertainty to be embedded from the outset or necessitate model reconstruction when new timing information becomes available, hindering iterative timing engineering. This paper presents a refinement-oriented timing specification framework built upon the Clock Constraint Specification Language (CCSL). It supports the progressive introduction of timing knowledge across three levels: logical timing relations, quantitative real-time constraints, and stochastic timing models. Instead of altering behavioural semantics, stochastic information is attached directly to timing quantities as a refinement. This enables implementation measurements and operational observations to be incorporated incrementally within a unified declarative framework. We implement our approach in an OCaml-based simulation tool and evaluate it on a simplified but representative Software-Defined Vehicle use case.
Journal refFDL 2026 - 29th Forum on specification and Design Languages, Sep 2026, Rome, Italy
