• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Symposium on Foundations of Health Informatics Engineering and Systems >An Event-B Approach to Timing Issues Applied to the Generic Insulin Infusion Pump
【24h】

An Event-B Approach to Timing Issues Applied to the Generic Insulin Infusion Pump

机译：一种综合胰岛素输注泵适应时间问题的事件-B

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

An insulin infusion pump (IIP) is a complicated and time critical control system. Making sure that the pump infuses insulin in conformance with a user's wishes and in conformance with safety related constraints, and does so at the right times, makes it a highly safety critical system. This paper uses Event-B to specify a generic model for an IIP, based on requirements developed by the US Food and Drug Administration (FDA). The IIP is an active and reactive control system. Each transition between states of the model is modelled as an event. To correctly specify the IIP, we need a model of time and synchronization of events with time that is sufficiently rich to achieve our safety aims. We create several sets to model the activation times of different events and the union of these time sets defines a global time activation set. All the actions in an event are triggered only when the global time matches the time specified in the event. When the action is activated, the time is deleted from the corresponding time set, but not the corresponding global time set. A time point is deleted from the global time set only when there are no pending actions for that time point. We are able to demonstrate that the resulting specification satisfies relevant required safety constraints.
机译：胰岛素输液泵（IIP）是一种复杂和时间的关键控制系统。确保泵符合用户的愿望和安全相关约束，并在正确的时间内符合胰岛素，使其成为一个高度安全的关键系统。本文根据美国食品和药物管理局（FDA）的要求，使用Event-B指定IIP的通用模型。 IIP是一个主动和无功控制系统。模型的状态之间的每个转换都被建模为事件。要正确指定IIP，我们需要一个时间和同步的时间和同步，时间足以实现我们的安全目标。我们创建了多个集合来模拟不同事件的激活时间，并且这些时间集的结合定义了全局时间激活集。只有在全局时间匹配事件中指定的时间时，才会触发事件中的所有操作。激活动作时，从相应的时间集中删除时间，但不是相应的全局时间集。只有当该时间点没有挂起的操作时，才会从全局时间删除时间点。我们能够证明所产生的规格满足相关所需的安全约束。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号