Experiences using lightweight formal methods for requirements modeling

摘要: The paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. differ from previously reported applications that were applied very early engineering process validate evolving requirements. results fed back into projects improve informal specifications. For each study, we describe what applied, how they much effort was involved, and findings were. In all cases, enhanced existing verification validation processes by testing key properties helping identify weaknesses. We conclude benefits gained unstable more than outweigh needed maintain multiple representations.