Creation and evaluation of formal specifications for system-of-systems development

摘要

Studies have suggested that formal specifications and lightweight formal methods help improve the clarity and precision of the requirements specification. This paper describes a process to augment the current informal approaches to system-of-systems development by introducing temporal assertions to capture the safety-critical and mission-essential system requirements and runtime model checking to evaluate the system designs and implementation. The process allows users to develop and validate temporal assertions iteratively via simulation with multiple scenarios, and to use the assertions to automate the testing of the system-of-systems under development as well as armor-plating the target system against any unexpected behaviors at runtime.