A. Dasso (Argentina) and C. George (Macao)
: Software Engineering, Formal Methods, RAISE, PVS, proof, logic,
We provide here an example of automated software en gineering by describing some of the problems confronted when trying to improve a set of tools supporting software development. The RAISE toolkit lacked a proof tool. This has been provided by writing a translator from RSL to PVS so that the PVS proof checker can be employed. This pa per discusses the problems that arise because of the dif ferences in the logics of RSL and PVS. It shows how the range of RSL specifications that can be translated soundly is increased through the novel technique of the generation of acceptability conditions as lemmas.
Important Links:
Go Back
