Using PVS to prove properties of systems modelled in a synchronous dataflow language

We report on our experience with using the PVS theorem prover as a verification tool for analyzing systems modelled in RSML^-e - a synchronous dataflow language. RSML^-e is a formal specification language particularly well-suited for specifying requirements of reactive systems. We advocate a specification-centered approach to system development, in which various development activities like prototyping, analysis, verification, testing, and code-generation are based on a formal model of the system requirements. To support the analysis and verification activities, we developed a translator from RSML^-e to PVS as part of our toolset. We used these tools to successfully verify properties of the mode logic of a flight-guidance system specified in RSML^-e by our industrial partner, Rockwell Collins Inc. The results from this exercise are encouraging. This paper describes our approach to formalizing RSML^-e in PVS and discusses briefly the strategies adopted in proving properties as well as some experiences.