Low-Effort Specification Debugging and Analysis
- Creators
- Ehlers, RĂ¼diger
- Raman, Vasumathi
Abstract
Reactive synthesis deals with the automated construction of implementations of reactive systems from their specifications. To make the approach feasible in practice, systems engineers need effective and efficient means of debugging these specifications. In this paper, we provide techniques for report-based specification debugging, wherein salient properties of a specification are analyzed, and the result presented to the user in the form of a report. This provides a low-effort way to debug specifications, complementing high-effort techniques including the simulation of synthesized implementations. We demonstrate the usefulness of our report-based specification debugging toolkit by providing examples in the context of generalized reactivity(1) synthesis.
Additional Information
V. Raman is supported by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA.Attached Files
Published - 1407.5399v1.pdf
Files
Name | Size | Download all |
---|---|---|
md5:fa21216803c0f50abcdaa7000ec27ce9
|
148.2 kB | Preview Download |
Additional details
- Eprint ID
- 52514
- Resolver ID
- CaltechAUTHORS:20141209-144837376
- TerraSwarm
- STARnet
- Microelectronics Advanced Research Corporation (MARCO)
- Defense Advanced Research Projects Agency (DARPA)
- Created
-
2014-12-10Created from EPrint's datestamp field
- Updated
-
2023-06-02Created from EPrint's last_modified field