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. © Springer-Verlag 2003.
CITATION STYLE
Rayadurgam, S., Joshi, A., & Heimdahl, M. P. E. (2003). Using PVS to prove properties of systems modelled in a synchronous dataflow language. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2885, 167–186. https://doi.org/10.1007/978-3-540-39893-6_11
Mendeley helps you to discover research relevant for your work.