Scholarlink

Timed automata due to Rajeev Alur and David Dill are the primary model for verifying properties of real-time systems with a continuous time domain. UPPAAL developed by Kim G. Larsen and Wang Yi and their collaborators is the main tool for practically performing such verifications. However, timed automata are in general not implementable. An automata model that enables implementation on the platform of Programmable Logic Controllers are PLC-Automata introduced by Henning Dierks. By translating them into timed automata, properties of PLC-Automata can be verified. We show this for properties formulated by counterexample formulas. The presentation is based on our book “Real-Time Systems” with Henning Dierks.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Verifying PLC-Automata Against Counterexample Formulas Using Timed Automata

  • 章节

  • 发表日期：

    2025年

查看全文
  • Ernst-Rüdiger Olderog

摘要

Timed automata due to Rajeev Alur and David Dill are the primary model for verifying properties of real-time systems with a continuous time domain. UPPAAL developed by Kim G. Larsen and Wang Yi and their collaborators is the main tool for practically performing such verifications. However, timed automata are in general not implementable. An automata model that enables implementation on the platform of Programmable Logic Controllers are PLC-Automata introduced by Henning Dierks. By translating them into timed automata, properties of PLC-Automata can be verified. We show this for properties formulated by counterexample formulas. The presentation is based on our book “Real-Time Systems” with Henning Dierks.