TY - JOUR
T1 - Using PVS to prove properties of systems modelled in a synchronous dataflow language
AU - Rayadurgam, Sanjai
AU - Joshi, Anjali
AU - Heimdahl, Mats P.E.
PY - 2003
Y1 - 2003
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0345687155&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0345687155&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-39893-6_11
DO - 10.1007/978-3-540-39893-6_11
M3 - Article
AN - SCOPUS:0345687155
SN - 0302-9743
VL - 2885
SP - 167
EP - 186
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -