Lowering the Barrier to Formal Modeling and Analysis

No ratings

Presented at High Confidence Software and Systems Conference 2022 by

Daniel Balasubramanian

Recent years have seen a significant increase in the application of formal methods to industrial systems. While this increase has been encouraging, there are still many tools which could provide practical, real-world benefits but that are impeded due to usability issues. These include packaging and installation issues, a lack of tooling integrated into traditional developer workflows, and limited visibility into automatedreasoning capabilities. This presentation will describe ongoing work in integrating our formal modeling framework, FORMULA, into traditional developer workflows and our efforts to make it more accessible to end users. FORMULA is a language and tool for formally specifying domain-specific languages (DSLs) and checking properties of those languages. We will describe our experience providing multi-platform support for Linux, Mac, Windows, and the Web, our packaging experience with Nix, language integration into multiple editors using the tree-sitter parser tool, and the design of a notebook-style interface for interacting with FORMULA’s automated reasoning capabilities. Our presentation will be framed in the context of our team’s participation in the DARPA Verified Security and Performance Enhancements for Large Legacy Systems (V-SPELLS) program, where we use FORMULA for compositional DSL programming and cross-domain reasoning.