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.