Temporal Specifications For Online Security System Monitoring and Synthesis

软件、硬件和嵌入式系统设计正在发生变化，以满足不断变化的需求。 下一代系统将以连接和反应的方式运行，这对适用于独立环境的系统和设计提出了挑战。例如，分布式医疗保健网络必须能够可靠和安全地传输医疗信息;医疗设备中的各种组件需要互操作，以实现所需的设备功能;网络信息的流传输质量需要对不断变化的系统输入做出持续反应。 由于系统组件必须以时间敏感和安全的方式运行，因此必须精确描述和分析它们的运行，以确保它们满足其运行要求。现在已经确定，正式的自动化分析技术适用于设计和分析安全和业务关键系统。 然而，全自动技术的应用在实践中可能存在问题。首先，即使是中等规模的系统设计也可能无法使用当前的全自动化技术构建，因为描述所有可能系统行为的底层状态空间可能非常巨大。 其次，许多当前的自动化设计技术更适合用于设计单片而不是分布式多组件系统设计。

Software, hardware and embedded system designs are changing to meet changing demands. Next generation systems will operate in a connected and reactive manner that challenges systems and designs that were suitable in standalone environments. For instance, distributed health care networks must be able to reliably and securely transmit medical information; the various components in medical devices require inter-operation in order to implement the desired device functionality; the streaming quality of network information requires ongoing reaction to changing system inputs. Because system components must operate in a time sensitive and secure fashion their operation must be precisely described and analyzed to ensure they meet their operational requirements. It is now well established that formal, automated analysis techniques are appropriate for designing and analyzing safety and business critical systems. However, application of fully automated techniques can be problematic in practice. First, even modestly sized system designs may be infeasible to build with current fully automated techniques as their underlying state spaces describing all possible system behaviors can be huge. Second, many current automated design techniques are more appropriately used to design monolithic rather than distributed multi-component system designs.