Rayadurgam, SanjaiJoshi, AnjaliHeimdahl, Mats2020-12-102020-12-102003In Proc. of the 5th International Conference on Formal Engineering Methods (ICFEM)https://hdl.handle.net/11299/217335Associated research group: Critical Systems Research GroupWe 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.Report