Cooperating Formal Methods Final Report

摘要

Formal methods research has developed a variety of mathematical tools andtechniques applicable to the development of software systems, but they are greatly underused. The reasons include the limited mathematical backgrounds of many end-users and developers; idiosyncratic support tools; lack of attention to technology transfer. We have developed a prototype formal methods interface (PMI) that permits different kinds of users, with different degrees of expertise, to cooperate in applying formal methods to define, explore, and analyze system designs and specifications. Systems are specified in RSML, a mixed graphical and textual notation for defining state machines. The FMI allows a user to perform