University of Minnesota
Software Engineering Center
/

You are here

Using PVS to Prove Properties of Systems Modelled in a Synchronous Dataflow Language

Date of Publication: 
November 2003
Associated Research Groups: 
Publication Files: 
Abstract: 
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.
Venue: 
In Proc. of the 5th International Conference on Formal Engineering Methods (ICFEM)
bibtex: 
@INPROCEEDINGS{Rayadurgam03:pvs, AUTHOR = "Sanjai Rayadurgam and Anjali Joshi and Mats P.E. Heimdahl", TITLE = "Using {PVS} to Prove Properties of Systems Modelled in a Synchronous Dataflow Language", BOOKTITLE = "Proceedigns of the 5th International Conference on Formal Engineering Methods, ICFEM 2003", YEAR = "2003", pages = "167-186", address = "Singapore", month = "November" }