Behavioral consistency checking between requirements and implementations

Checking if the implementations conform to the requirement models is challenging. Most existing techniques for consistency checking either focus on requirement models (e.g., requirements consistency checking), or on the implementations (e.g., code-based testing) only. In this paper we propose an approach to checking behavioral consistency of implementations against requirement models directly to overcome these limitations. Our approach extracts two behavioral models represented by Labelled Transition Systems(LTS) from requirement models and implementations respectively, and checks the behavioral consistency between these two models based on behavioral simulation relation of LTS. The checking results of our approach provide evidence for behavioral inconsistency as well as inconsistent localization. A research prototype called BCCH and a case study are presented to give initial validation of this approach.