Symbolic Model Checking Property Specification Language Seminars/Workshops

Abstract

PSL is a specification language which has been accepted as an industrial standard. In PSL, SEREs are used as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. Then, we extend the LTL symbolic model checking algorithm to that of APSL, and then present a tableau based APSL verification technique, which can be implemented via BDD based symbolic approach. Moreover, we implement an extension of NuSMV, which supports symbolic model checking of APSL. The experimental results show that APSL can be efficiently verified.