首页/论文/1905.09458

arXiv 1905.094582019-05-23cs.SEcs.FL

使用参数时间自动机形式化Time4sys

Formalizing Time4sys using parametric timed automata

Étienne André

备注：: This is the author (and slightly extended) version of the manuscript of the same name published in the proceedings of the 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019)
DOI：: 10.1109/TASE.2019.00031

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

关键的实时系统必须经过验证，以避免在出现故障时造成严重后果的风险。泰利斯开发了一个开放的形式主义Time4sys模型实时系统，具有表达功能，如周期性或零星的任务，任务依赖性，分布式系统等，但是，Time4sys不允许原生的正式推理。在这项工作中，我们提出了一个翻译从Time4sys（参数）时间自动机，以便允许一个形式化验证。

英文摘要：

Critical real-time systems must be verified to avoid the risk of dramatic consequences in case of failure. Thales developed an open formalism Time4sys to model real-time systems, with expressive features such as periodic or sporadic tasks, task dependencies, distributed systems, etc. However, Time4sys does not natively allow for a formal reasoning. In this work, we present a translation from Time4sys to (parametric) timed automata, so as to allow for a formal verification.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Timed I/O Automata：完善你的时序规范理论永远不会太晚

Timed I/O Automata: It is never too late to complete your timed specification theory

本文提出基于 Timed I/O Automata 与 Timed I/O Transition Systems 的完整实时系统规范理论，涵盖精化、一致性、组合、商等构造，并由严格证明和 ECDAR 工具实现支持。

2023-07-13cs.FLcs.SE

TarTar：一个时间自动机修复工具

TarTar: A Timed Automata Repair Tool

我们提出了TarTar，一个自动修复分析工具，给定的定时诊断跟踪（TDT）的时间自动机模型的模型检验过程中获得的，建议可能的语法修复的分析模型。建议的修复包括修改位置不变量和转换保护中的时钟边界值，添加或删除时钟重置等。建议的修复保证消除给定TDT的可执行性，同时保留系统的整体功能行为。我们深入研究了TarTar的设计和架构，并表明它可以成功修复来自不同案例研究的系统模型中69%的种子错误。

2020-05-12cs.FLcs.SE

基于tock-CSP到时间自动机自动转换的时态推理

Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata

在这项工作中，我们考虑将tock-CSP转换为UPPAAL的时间自动机，以便于使用UPPAAL在推理tock-CSP模型的时间规范。进程代数tock-CSP提供了离散时间行为建模的文本符号，并支持自动验证工具。类似地，UPPAAL实时验证工具箱\uppaal支持使用图形符号自动验证时间自动机（TA）。这两种建模方法，TA和tock-CSP，在建模和验证方法，时序逻辑和细化，分别不同，以及它们提供的自动验证设施。例如，活性要求很难用tock-CSP的结构来指定，但它们很容易在UPPAAL中指定和验证。为了利用时序逻辑，我们翻译tock-CSP到TA的\uppaal，我们已经开发了一个翻译技术和它的支持工具。我们提供的规则，翻译tock-CSP到一个网络的小TA捕捉的组成结构的tock-CSP，是不可用的TA。为了验证，我们从一个实验方法的基础上有限逼近跟踪集。然后，我们探索数学证明，以建立覆盖无限迹的规则的正确性。

2021-04-27cs.FLcs.SE

使用控制自动机形式化安全需求

Formalizing Safety Requirements Using Controlling Automata

安全性是可靠性的一个重要因素。它被定义为没有事故。大多数涉及软件密集型系统的事故都是系统事故，这是由不安全的系统间或组件间交互引起的。为了验证不存在与功能失调的交互相关的系统危害，工业界呼吁对系统安全需求和组件之间的交互约束进行建模的方法。本文提出了这样一种形式主义，即接口控制系统（或简称C-Systems）。接口C系统由接口自动机和控制自动机组成，在Meta级上形式化安全交互并约束系统行为。该框架不同于传统的模型检验框架。它明确地分离了产品工程师和安全工程师的任务，并提供了一种自顶向下的技术，用于对具有安全约束的系统进行建模，并自动组成符合安全要求的安全系统。这项工作的贡献包括正式的安全要求和自动确保系统安全的方式。

2009-05-14cs.FLcs.SE

考虑连续时间语义的时间自动机上的MITL公式

Verifying MITL formulae on Timed Automata considering a Continuous Time Semantics

时间自动机（TA）实际上是一种标准的建模形式主义，当人们感兴趣的是随着时间的推移分析它们的行为时，它可以表示系统。这种建模形式主义主要用于检查系统的行为是否满足一组感兴趣的属性。即使存在时间自动机的有效模型检查器，这些工具也不容易配置。首先，它们的设计并不容易允许添加新的时间自动机构造，例如新的同步机制或通信过程，但它们假设一组固定的时间自动机构造。其次，它们通常不支持完整的度量间隔时态逻辑（MITL），并且依赖于逻辑的精确语义，其中指定了不能容易地修改和定制的感兴趣的属性。最后，它们不容易允许在不同的上下文中使用可以加速验证的不同求解器。本文提出了一种新的技术来执行模型检验的完整的度量区间时序逻辑（MITL）属性TA。该技术依赖于翻译的TA和MITL公式到一个中间的约束LTL的时钟（CLTLoc）公式，这是通过一个可用的决策过程进行验证。该技术是灵活的，因为中间逻辑允许编码新的语义以及新的TA结构，只需添加新的CLTLoc公式。此外，我们的技术不受特定求解器的约束，因为中间CLTLoc公式可以使用不同的程序进行验证。

2019-09-10cs.FLcs.LOcs.SE

定价时间自动机网络的随机语义和统计模型检验

Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata

本文提出了一种基于组件竞争的定价时间自动机网络的自然随机语义。语义提供了满足概率加权CTL属性（PWCTL）的基础上，保守地扩展了经典的时间自动机满足TCTL。特别是扩展允许硬实时性能的时间自动机表达在TCTL的性能属性，例如，在概率保证的时间和成本有界的属性。本文的第二个贡献是统计模型检验（SMC）的应用程序，有效地估计正确性的非嵌套PWCTL模型检验问题与所需的置信水平，根据一些独立运行的NPTA。除了应用经典的SMC算法，我们还提供了一个扩展，允许有效地比较性能特性的NPTA在参数设置。第三个贡献是一个有效的工具实现我们的结果和应用程序的几个案例研究。

2014-11-28cs.SE

更多相关论文收起更多论文

基于时间自动机形式化建模与验证的数字公路法规

Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata

设计安全、可靠和值得信赖的自动驾驶汽车（AV）的挑战之一是确保AV遵守交通规则。为此，自动驾驶汽车需要能够理解和推理交通规则。在以前的工作中，我们引入了空间交通逻辑USL-TR，允许明确的，机器可读的，形式化的交通规则。这只是迈向可验证地遵守交通规则的自主交通代理的第一步。在本研究预览中，我们重点关注两个进一步的步骤：a）直接从交通规则中检索行为图，b）将行为图转换为使用USL-TR公式的时间自动机。有了这个，我们就有了一个正式的交通规则代表，并可以朝着建立数字公路代码的方向迈进。我们简要地设想进一步的步骤，其中包括添加环境和代理模型的时间自动机，最终实现和验证这些交通规则模型使用选择的形式化验证工具。

2022-09-28cs.FLcs.LOcs.SE

基于遗传编程的时间自动机学习

Learning Timed Automata via Genetic Programming

近年来，模型学习得到了越来越多的关注。它从黑箱系统的测试数据中导出行为模型。这种技术的主要优点是，它们能够在不访问系统内部的情况下进行基于模型的分析。应用范围从模型检验的全自动测试到系统理解。目前的工作重点是学习有限状态机的变化。然而，大多数技术考虑离散时间。在本文中，我们提出了一种学习时间自动机，有限状态机扩展与实值时钟的方法。该学习方法生成与通过测试收集的一组定时轨迹一致的模型。这一代是基于遗传编程，搜索为基础的技术自动程序创建。我们评估我们的方法对44个定时系统，包括四个系统从文献和40个随机生成的例子。

2019-02-15cs.SE

Timed k-Tail：时间自动机的自动推理

Timed k-Tail: Automatic Inference of Timed Automata

在实践中，描述软件系统性能的精确的和最新的模型很少。为了解决这个问题，软件工程师可以使用规范挖掘技术，它可以自动导出捕获分析中系统行为的模型。到目前为止，大多数规范挖掘技术都集中在系统的功能行为上，特别强调表示操作顺序的模型，如时态规则和有限状态模型。尽管这些模型很有用，但它们本质上是不完整的。例如，它们错过了定时行为，这与许多类系统和组件（如共享库和用户驱动的应用程序）极其相关。挖掘包括功能和时序方面的规范可以提高许多测试和分析解决方案的适用性。本文解决了这一挑战，提出了时间的k-Tail（TKT）规范挖掘技术，可以挖掘时间自动机从程序的痕迹。由于时间自动机可以有效地表示系统的功能和时间行为之间的相互作用，TkT可以在与时间相关的信息相关的情况下被利用。我们的实证评估表明，TkT可以有效地挖掘准确的模型。挖掘出的模型已被用于识别具有异常时间的执行。评估表明，大多数的异常执行已被正确识别，而产生的误报很少。

2017-05-23cs.SE

可视化电子合同的时间自动机语义

Timed Automata Semantics for Visual e-Contracts

C-O图作为一种更直观地表示电子合同的手段而被引入，其中可以表示不同签署人的义务、许可和禁止，以及在不履行其义务和禁止的情况下的处罚。在这样的图中，我们也能够表示绝对和相对的时间约束。在本文中，我们提出了一个正式的语义C-O图的基础上扩展的状态和边缘的顺序，以表示不同的道义模态的时间自动机。

2011-09-13cs.LOcs.SE

定时I/O自动机的组合活性保持约束测试--技术报告

Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata -- Technical Report

I/O一致性测试理论（例如，ioco）关注的是正式定义实现的可观察输出行为何时符合规范允许的行为。因此，人们提出了几种ioco的实时扩展，通常称为tioco，进一步考虑了动作之间允许的延迟。在本文中，我们提出了一个改进版的tioco，称为实时ioco（ltioco），解决现有定义的各种弱点。在这里，一个合理的适应静止（即，任何输出的可观察到的不存在）到实时行为的转换必须小心进行：因此，LTIOCO将允许发生的安全输出与强制在特定时间段内发生的实况输出区分开，从而引起静止的两个不同方面。此外，tioco经常被定义在时间I/O标记转换系统（TIOLTS），时间I/O自动机（TIOA）的语义模型，这是无限分支，因此不可行的实际测试工具。相反，我们扩展了理论的区域图，使有限的语义模型TIOA的ltioco测试。最后，我们调查ltioco的组合性与平行组成，包括适当的治疗沉默的过渡。

2019-09-10cs.FLcs.LOcs.SE

从规范模型到解释模型：时间自动机的一种提取和精化过程

From Specification Models to Explanation Models: An Extraction and Refinement Process for Timed Automata

自主系统控制着我们日常生活中的许多任务。为了增加对这些系统的信任和人类与自主系统之间互动的安全性，应向用户、专家和公共当局解释系统行为和自主决策的理由。提供这种解释的一种方法是使用行为模型在运行时生成特定于上下文和用户的解释。然而，这是以更高的建模工作为代价的，因为需要构建更多的模型。在本文中，我们提出了一个高层次的过程中提取系统模型的解释模型，并随后细化这些对特定的用户，解释的目的和情况。通过这一点，我们使规范模型的重用集成到系统的自我解释能力。我们使用自动驾驶领域的一个运行示例来展示我们的方法。

2022-09-28cs.FLcs.LOcs.SE