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 ...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.展开更多
基金Supported by the National Natural Science Foundation of China(91118003,61003071)the Fundamental Research Funds for the Central Universities(3101046,201121102020006)the Special Funds for Shenzhen Strategic New Industry Development(JCYJ20120616135936123)
文摘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.
