Abstract: This paper uses live sequence chart (LSC) to describe scenariobased requirement specifications. According to the principle that design model must be consistent with the specification of requirement model, and aiming at extraction of safety, reachability and liveness, the paper proposes three criteria for generating and extracting properties from LSC specification automatically. The extracted result can be used for automatic verification, providing protection for consistency of requirement model with the design model.

Key words: consistency, extracting properties, live sequence chart (LSC), model checking