Using Statechart Assertion for the Formal Validation and Verification of a Real-Time Software System: A Case Study

摘要

Verification and validation (V&V) is one of the software engineering disciplines that helps build quality into software. V&V comprehensively analyzes and tests software to determine that it performs its intended functions correctly, and ensures that it does not perform unintended functions. However, V&V traditionally relies on manual examination of software requirements, design artifacts and the systematic or random testing of target code. As software-intensive systems become increasingly complex, traditional V&V techniques are inadequate for locating subtle errors in the software. It is even more challenging to test embedded real-time systems characterized by temporal behavior. For the past several decades, academia has actively researched the use of formal methods that help improve the quality of the software. Nonetheless, the techniques developed using formal methods still are not widely accepted in industry and in government. Professor Doron Drusinsky from Naval Postgraduate School (NPS) has developed a novel lightweight formal specification, validation and verification technique. The technique is focused on modeling reactive real-time systems with UML-based formal specifications and log file based Runtime Verification (RV). This thesis presents a case study as a proof of concept in support of this V&V technique, applied on a complex, already developed and fielded mission-critical system. It has successfully demonstrated a pragmatic approach in achieving a high quality V&V testing.