TRACE: Toolkit for Requirements Analysis, Capture, and Elicitation
摘要
Verification and validation of requirements is a crucial step in Model-Based Engineering to avoid costly re-work involved in the re-design and re-validation of systems and software due to flawed requirements. Verification of requirements necessitates capturing them in a formal notation that is amenable to analysis by formal methods tools. Further, realistic systems specify requirements cutting across subsystems that involves multi-physics interactions of subsystems’ properties of interest. Such multi-domain requirements also constrain the design space of sub-systems. We present TRACE (Toolkit for Requirements Analysis, Capture, and Elicitation) for systems that allows for the capture of different types of requirements. TRACE facilitates the analysis of system requirements including a wide variety of analyses such as conflict, independence, contingency, and completeness analyses available in several practical requirements analyses tools. In addition, requirements regarding component properties may also be formalized as guarantees and checked for implication by other requirements using backend Satisfiability Modulo Theories (SMT) solvers. Detailed diagnostic information for failed guarantees, including UNSAT cores and counterexamples, will be provided to assist users in pinpointing and resolving the identified issues. We apply TRACE to an industrial Hybrid Electric Propulsion System (HEPS) use case, showcasing various capabilities.