EXPERIENCES USING LIGHTWEIGHT FORMAL METHODS FOR REQUIREMENTS MODELING

This paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault prote ction systems. The case studies differ from previously reported applic ations of formal methods in that formal methods were applied very earl y in the requirements engineering process, to validate the evolving re quirements. The results were fed back into the projects, to improve th e informal specifications. For each case study, we describe what metho ds were applied, how they were applied, how much effort was involved, and what the findings were. In all three cases, formal methods enhance d the existing verification and validation processes, by testing key p roperties of the evolving requirements, and helping to identify weakne sses. We conclude that the benefits gained from early modeling of unst able requirements more than outweigh the effort needed to maintain mul tiple representations.