Lowering the Barrier to Formal Modeling and Analysis
| Abstract: 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.
Dr. Daniel Balasubramanian
is a Senior Research Scientist at the Institute for Software Integrated Systems and an Adjunct Associate Professor in the School of Engineering at Vanderbilt University. He is currently the PI on the DARPA Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) program, and he was a co-PI on the DARPA Space-Time Analysis for Cybersecurity (STAC) program. He is currently the PI on an NSF Smart and Connected Communities project, and he has research experience on a multitude of projects including the Model-Based Integration of Embedded Systems (MoBIES) project, the DARPA Producible and Adaptable Model-based Software (PAMS) project, the NASA Model-Transformation and Verification project, the DARPA Instant Foundry Adaptive through Bits project, the AFRL Resilient Software Systems (ReSoS) project, the DARPA META project, and model-based development tools from Microsoft Research, during which time he was supported by a grant from Microsoft Research. Dr. Balasubramanian is particularly interested in analysis for modeling languages.