Formal Methods at Scale (FMaS)
Abstract
The Formal Methods at Scale (FMaS) program will create new mathematical methodologies, techniques, and tools for proving and providing evidence of correctness for software systems whose size and complexity renders their modeling and analysis infeasible with current techniques. Formal methods are techniques for reasoning about and proving various properties for software code or design models, generally focusing on logical relationships that connect specifications and models with executable code. A key to scalability is to focus more narrowly on particular quality or functional attributes, such as security and safety, rather than address all features and functions of the components of a software system. A second key to scalability is to provide for composability, which enables trustworthy components to be efficiently assembled into trustworthy systems. The FMaS program will accelerate this new scalable formal methods paradigm by extending formal methods techniques, tools, and practices along several dimensions, including (1) the range of properties and qualities that are modeled and reasoned about, such as relating to security, safety, performance, fault tolerance, and real-time, (2) the complexity and the size of systems and their supply chains, including issues related to composability, (3) efficiency of formal methods-related modeling, tooling, and engineering practices, including more natural integration into mainstream tooling and practices, (4) ability to rapidly co-evolve systems and associated evidence, for example to respond to rapid evolution of threats and associated mission concepts, and (5) ease of use for non-expert developers and evaluators. FMaS aims to create formal methods applicable to software systems of the size and complexity commonly encountered in military and civilian mission-critical systems, and to speed the adoption of these methods into practice and tooling.
Document Details
- Document Type
- Accomplishment
- Publication Date
- Oct 01, 2021
- Source ID
- 717c4e656b15d120e239d0ce847f795b