Verification of Scenario-Based Safety Requirement Specification on Components Composition

For the development of component-based safety critical systems, not only consistency and compatibility among component interfaces, but also safety requirements of system need to be verified after components composition. This paper proposes a light-weight formal verification framework focusing on industry application, safety requirements specification through graphical PSC(Property Sequence Charts), components interface behavior model with LTS(labeled transition system). By proving that the PSC semantic can be transformed into linearization sequences set, we present the translation algorithm from PSC to image LTS. Thus, safety requirement specifications can be verified by model checking and be implemented by LTSA tools.