Retrospective exploration of safety properties in real-time concurrent systems

Describes using cascading of two existing tools: Hyperbook for source code analysis to facilitate software understanding, and PARAGON, for static analysis of safety-critical real-time systems. The goal is to provide an efficient and scalable toolset that minimizes human interaction during analysis. The toolset operates directly on source code without the need for the user to come up with initial or intermediate specification. Such a specification is constructed automatically during the analysis. The toolset is applicable to analysis of legacy software as well as to validation of new software. It is oriented towards exhaustive static analysis of software, without resorting to simulation. The source code together with the description of its architecture and environment are presented as input. Hyperbook produces a set of state machines that represent the static view of the code. The state machines serve as input to PARAGON. PARAGON reports interleaved events, which are used for software understanding and testing. It can detect flaws such as whether deadlocks are possible or if any catastrophic events may occur. PARAGON can produce diagnostic information that is used to identify the source of the problem. A major concern in software reengineering is the size of the source software. Hyperbook partitions the source code into software units that conform with the given architectural view. PARAGON´s formal analysis is performed in a modular and hierarchical fashion