Software Implementation from Rigorous Formal Usable Requirements (SIRFUR)

The Software Implementation from Rigorous Formal Usable Requirements (SIRFUR) project will develop and deploy model-based system engineering (MBSE) tools to provide formal verification evidence that system-level safety and security requirements represented in system models are accurately reflected in the subsystem components and the code that implements them.  SIRFUR will autogenerate embedded C code to align that component interfaces, the application code that implements those interfaces, and the component's run-time environment in a formally verifiable way.  The departure point for SIRFUR combines the error analysis developed on SSCATE Phase II, Kansas State University's Logika Integrated Verification Environment, the AADL representation of run-time semantics for thread dispatch and inter-process communications developed under the DARPA Cyber Assured System Engineering (CASE) project, and code generation technology to add cyber resiliency to software intensive systems by targeting separation kernels prototyped on the Department of Homeland Security (DHS) ISOSCELES program and matured on CASE.  SIRFUR will also leverage an existing MBSE process also in use today by the U.S. Army called the Architecture Centric Virtual Integration Process (ACVIP).  The work will be demonstrated in the context of a CubeSat, a non-trivial system with interacting, mixed-criticality subsystems. This will provide a realistic test case that relies on significant software functionality, as well as the correct interaction of a diverse mix of software, hardware, and mechanical subsystems, similar to that required for many DoD systems. SIRFUR will be deployed as part of Adventium's Curated Access to Model-based Engineering Tool (CAMET) Library, an existing collection of model-based systems engineering (MBSE) tools in use today. SIRFUR combines previous work on the SSCATE SBIR with work from several other programs, including CASE. SIRFUR will increase confidence that the implemented code correctly reflects its model-based specification, providing a formal correspondence between the analyses performed on the models and what is deployed in the real system.