Software verification is a so tedious process that only trivial system can be handled manually. So automated techniques are needed for verifying complex software. Compositional Reachability Analysis (CRA) is a verification technique that can be readily automated for Labelled Transition System (LTS). Labels of LTSs represent the possible actions of the system. It makes use of the structure of a system and constructs the global system by composing the LTSs of a system successively from that of its components, hiding unobservable actions at each stage. Validations can be made against those system properties with actions that are retained at the global system behaviour. CRA is effective when few actions of the system need to be made globally observable. As such, it is not effective to analy...[ Read more ]

Software verification is a so tedious process that only trivial system can be handled manually. So automated techniques are needed for verifying complex software. Compositional Reachability Analysis (CRA) is a verification technique that can be readily automated for Labelled Transition System (LTS). Labels of LTSs represent the possible actions of the system. It makes use of the structure of a system and constructs the global system by composing the LTSs of a system successively from that of its components, hiding unobservable actions at each stage. Validations can be made against those system properties with actions that are retained at the global system behaviour. CRA is effective when few actions of the system need to be made globally observable. As such, it is not effective to analyse properties involving many unobservable actions because they have to be made globally observable before checking can be conducted.

To address these problems, we propose a framework to check safety property with CRA. This mainly consists of two parts: Pruned Compositional Reachability Analysis (PCRA), and Propagating Composition. PCRA constructs a trimmed down version of compositional hierarchy, which captures the desired actions of in safety property, and generates a global system. Propagating Composition composes property automaton with higher-level processes successively to detect violation of safety property.

There are several advantages of the new techniques. First, the computational time to generate the required global system is amortised over multiple property checking tasks, which lower the total computational cost. Second, violations can be detected at an early stage of checking. A production cell system designed by the Forschungszentrum Informatik is used as a case study. It consists of thirty non-trivial concurrent processes. Twenty-four safety properties have been checked against the system. The result shows a significant reduction of checking time compared to conventional CRA.