Generative AI for Rigorous Digital Engineering
Rigorous Digital Engineering (RDE) is an engineering process and methodology created and refined over the past two decades by this author, first during his days as a Professor, and over the past decade while a Principal Scientist at Galois. RDE combines the practical use of Model-Based Engineering (MBE) with Applied Formal Methods (AFM) in such a way that formality is hidden from engineers using a technique called Secret Ninja Formal Methods (SNFM). RDE has been demonstrated on hundreds of software and hardware systems, and has been used on dozens of Galois projects to create secure, high-assurance software systems and ASICs. The kinds of engineering that have been incorporated into RDE include systems, software, firmware, hardware, safety, and security engineering.
Galois has been experimenting with using untrustworthy AI as partners in nearly every facet of Rigorous Digital Engineering. The facets include doing domain engineering, requirements engineering, security engineering, systems engineering, model-based engineering and design at the source code level, product line engineering, software engineering and hardware engineering, building various kinds of assurance cases involving both runtime verification and testing for validation, and formal verification.
DARPA Space-BACN recently funded the development of an entire course on Rigorous Digital Engineering. The first edition of the course is now complete, and is initially being given internally at Galois. It is meant to be publicly available to the world this year. While the course comes with many historic example RDE projects (e.g., SHAVE and HARDENS), a wholly new RDE Course Demonstrator called ENGRAVE is being created by this author. ENGRAVE is an example RDE system that focuses on the design, development, and assurance of a domain-specific language (DSL) and architecture (DSA), including a family of programming and specification languages, and a full small development tool suite including a type checker, interpreter, testbench generator, and a formal verification tool.
This kind of case study is important because many modern DoD/DIB systems are beginning to use DSLs and DSAs more commonly, and thus including these kinds of components in the Dataset improves its utility. Also, ENGRAVE resembles many of the technologies that Galois creates in its R&D. Finally, the ENGRAVE project is one of the main places where we are experimenting with the use of modern AIs.
In only a few days of work, leveraging generative AIs and prototype LLM used as described above, I have already written: (0) the specific RDE process and methodology for the ENGRAVE project, (1) a CONOPS for the system, (2) a domain engineering model in the Lando system specification language, (3) system requirements, also in Lando, (4) designed the ENGRAVE family of languages, including its grammar and informal semantics, (5) a product line model describing the family of languages, command line options, CI/CD/CV system, and assurance case, (6) a system design sketch in UML and SysMLv2, (7) a set of grammars for the full language family, (8) the entire front-end of the tool flow including a lexer, parser, and intermediate representation, (9) a full container environment for CI, CD, and CV, (10) instantiated that CI/CD/CV environment with continuously measured metrics of system completeness and correctness, and (11) instantiated a set of standard developer environments using popular IDEs and command-line tools. Prior to HCSS taking place, I expect to complete the ENGRAVE demonstrator.
My HCSS talk will review modern AI as applied to RDE by walking through the ENGRAVE project.
Dr. Joe Kiniry has been a Principal Scientist at Galois for 10 years. He is also the Principled CEO and Chief Scientist of the public benefit corporation Free & Fair. He was previously an academic in Europe for twelve years, lastly as a Full Professor and Head of Section at the Technical University of Denmark. Joe has extensive experience in formal methods, the foundations of mathematics, information security, and high-assurance, model-based software, firmware, hardware, safety, security, requirements, and systems engineering---what we now call *Rigorous Digital Engineering*. He has over twenty years experience in the design, development, assurance, support, and auditing of nationally critical, safety-critical, and national security systems, including supervised and internet/remote electronic voting systems. He co-led the DemTech research group at the IT University of Copenhagen and has served as an adviser to the Dutch, Irish, Danish, and US governments in matters relating to electronic voting. He has lead as a Principal Investigator over $35M of R&D over the past twenty years and holds a PhD from the California Institute of Technology.