Time4sys2imi：一个在不确定性下形式化实时系统模型的工具
软件工程
2019-10-30 v1 计算机科学中的逻辑
摘要
Time4sys 是泰雷兹（Thales）开发的一种形式化方法，实现了实时系统的图形化规范。然而，该形式化方法不允许对实时系统进行形式化分析。因此需要将此工具翻译为具备形式化语义的形式化方法。我们在此介绍 Time4sys2imi，一个将 Time4sys 模型翻译为 IMITATOR 输入语言中的参数化时间自动机的工具。该翻译不仅允许检查实时系统的可调度性，还可推断一些保证可调度性的时序约束（例如截止时间、偏移量）。我们已成功将 Time4sys2imi 应用于多个示例。
引用
@article{arxiv.1907.13447,
title = {Time4sys2imi: A tool to formalize real-time system models under uncertainty},
author = {Étienne André and Jawher Jerray and Sahar Mhiri},
journal= {arXiv preprint arXiv:1907.13447},
year = {2019}
}
备注
This is the author (and extended) version of the manuscript of the same name published in the proceedings of ICTAC 2019. This work is supported by the ASTREI project funded by the Paris \^Ile-de-France Region, with the additional support of the ANR national research program PACS (ANR-14-CE28-0002) and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST