离散控制器综合在安全关键嵌入式系统中的应用

"这篇论文探讨了离散控制器综合在安全关键嵌入式系统中的应用，强调了使用形式化方法和容错技术对于确保系统安全的重要性。作者Alain Girault和Eric Rutten提出了一个利用离散控制器综合来构建安全执行系统的方案，该方案能够在故障发生时保证系统的正确性和功能实现。文章涵盖了周期性任务、分布式、异构和故障沉默处理器的模型，以及环境模型，用于描述可能的故障模式。此外，还介绍了使用Sigali符号DCS工具和模式自动机来实现这种方法。关键词包括离散控制器综合、容错和实时系统。" 离散控制器综合（Discrete Controller Synthesis，DCS）是一种将离散事件系统与控制理论相结合的技术，主要用于设计和分析控制系统。在安全关键嵌入式系统中，DCS有助于生成能够处理预期故障的控制逻辑，确保系统在各种条件下仍能保持其规定的行为。这些系统通常出现在航空航天、核能、汽车等领域，具有严格的实时性要求，即错过时间限制可能会导致严重后果。 嵌入式系统的特点包括双模态操作，即同时包含连续的自动控制（如微分方程建模的控制律）和离散事件（如模式切换）。此外，它们通常需要在有限的硬件资源下运行，这可能导致计算能力和内存的限制。为了应对这些挑战，系统可能采用分布式和异构架构，以提高计算能力并减少延迟。 安全设计方法的关键在于确保系统在处理器故障时仍能继续运行。通过使用DCS，可以创建一个冗余的、容错的系统，即使部分处理器失效，整体功能也能得到维持。这通常涉及到系统分配策略的优化，以确保即使在单点故障的情况下，关键任务仍然能够执行。 论文中提到的环境模型是用来描述系统可能遇到的各种故障模式，这有助于在设计阶段就预测和预防潜在问题。 Sigali符号DCS工具和模式自动机则是实现这种安全设计方法的具体工具，它们帮助设计者生成和验证控制策略，确保系统在面对故障时能够正确响应。 形式化方法在这一领域起着至关重要的作用，因为它们提供了一种精确描述系统行为和故障模型的方式，从而能够进行严格的形式验证。这种方法可以确保系统满足预定的安全和性能标准，减少因设计缺陷导致的故障风险。 这篇论文深入研究了如何利用离散控制器综合来设计安全关键的嵌入式系统，特别是在面临处理器故障和实时性需求时如何保证系统可靠性。通过形式化方法和特定的工具支持，这种方法为开发能够抵御故障的实时系统提供了有力的理论和技术基础。