Reactive Program Analysis From The Ground Up

点击翻译按钮获取中文摘要

Fully automated program analysis tools form the core of software tools used to provide assurance that current and next-generation hardware, software, and embedded systems meet their safety-critical requirements. However, too often the sheer size and complexity of the system models makes automated analysis infeasible, either due to cost or time requirements. In essence, this growth in system size is a byproduct of the fact that the systems under consideration are comprised of many interconnected components. Even if the individual components are of manageable size, the size of the combined systems may be enormous. To cope with this state explosion problem, a reexamination of the basic elements in the analysis is in order. This includes the compositional models used to build new systems; the interconnection architectures by which the components share information; the abstraction models used in place of the too large models under verification; the notions of equivalence used to compare the abstract models to the originals; and the specification language used to describe expected system behaviour. With the new elements in hand, fully automated analysis tools will be designed that are either capable of analyzing systems that were previously not amenable to fully automated analysis, or for which the cost of analysis was prohibitive. In particular, new notions of symmetry amongst process and composition of processes will be used to analyze the behaviour of communication protocols. Therefore the research will be of value in that it will enable fully automated safety assurance tools to be applied to critical systems, such as communication protocols or embedded controllers, that are currently beyond the scope of these tools. This will in turn increase confidence in the operation of these systems.