我正在为Haskell开发混合系统控制器。
FRP库(现在我使用的是netwire，但有几个很好的库和许多关于未来的有趣研究)为问题的连续时间方面提供了一个很好的解决方案。用信号名称、维度、首选单元等来扩充它们，使您的系统具有模块化、自描述性，并且具有对正确性的信心的直接途径。
我正在寻找资料，民间传说，或论文提供离散时间方面的类似性质。在某种意义上，这个问题要简单得多，因为状态机已经得到了很好的研究和简单。在其他意义上，它更困难，我将简要地解释如何。
正确性显然是最重要的，值得庆幸的是，它也很简单。
自我描述更成问题。你不仅希望控制器处于正确的状态，还希望它能够告诉你它处于什么状态。还有它是如何到达那里的。以及它接下来可能走向何方。所以你可以给所有东西加上名字，这是可行的，但它与模块化有些冲突。您还希望能够从简单的离散时间行为构建复杂的离散时间行为。但是当你问系统它处于什么状态时，通常高层次的答案比低层次的答案更有趣(或者至少一样有趣)。你怎么把它弄干净?我尝试过一些天真的方法，用不同的方式把自己裹在意大利面里，但似乎一定有优雅的解决方案吧?
我在自我描述方面遇到的另一个问题是，我希望有一个自我描述条件的列表(通常比较:它已经10秒了吗?我离下一个航路点还有三英尺吗?电池电量降到15%以下了吗?等)正在被监控的，可能会触发下一个状态转换。这里有一些棘手的问题，甚至是理想的语义，因为似乎这些事件中的一些是更好地处理"从下向上"(例如，您正在执行的任何低级步骤的预期终止条件)和一些"从上向下"(例如，设备故障检测，地理围栏，…)。即使你放松了自我描述的目标，这也会导致自己陷入困境。
除了诊断之外，这里准确的自我描述信息对于抽象解释也非常有用，通过猜测哪些事件可能在何时发生，将系统的状态投射到未来。许多事件条件导致它们自己产生相当简单的猜测(例如使用速度，燃料消耗率，计时器)。其他的更复杂，但可能仍然值得为一些应用程序开发预测(例如，来自运营商的预期订单、天气预报、移动目标的预测轨迹)。如果能找到一种设计，不仅用名称来注释条件，而且用函数来注释这类东西，那就太好了。
有谁有这方面的经验愿意分享吗?
好吧，所以我想说，你的问题的"真正"答案是，你所要求的一些东西是开放的研究领域——特别是我认为你想要的一些自我描述特征可能需要某种程度的"意大利面"，因为你试图解决的问题本质上是复杂的。
话虽如此，您对模块化的关注正是正确的方法。我会说，看看Keymaera，因为我相信它有你想要的功能，尽管它是在Java中。我还建议您查看Keymaera网站上的出版物页面，因为这将为您提供有关问题的宝贵见解。
如果你不喜欢Keymaera的方法，你也可以考虑使用定时自动机，这是另一种方向建模，应该足以满足你的问题描述。