Formal Specification Level: Towards Verification-driven Design Based on Natural Language Processing

Rolf Drechsler; Mathias Soeken; Robert Wille

In: Proceedings of the Forum on Specification & Design Languages 2012. Forum on Specification & Design Languages (FDL-2012), September 18-20, Vienna, Austria, IEEE, 2012.


The steadily increasing complexity of the design of embedded systems led to the development of both an elaborated design flow that includes various abstraction levels and corresponding methods for synthesis and verification. However, until today the initial system specification is provided in natural language which is manually translated into a formal implementation e.g. at the Electronic System Level (ESL) by means of SystemC in a time-consuming and error-prone process. In this paper, we envision a design flow which incorporates a Formal Specification Level (FSL) thereby bridging the gap between the informal textbook specification and the formal ESL implementation. Modeling languages such as UML or SysML are envisaged for this purpose. Recent accomplishments towards this envisioned design flow, namely the automatic derivation of formal models from natural language descriptions, verification of formal models in the absence of an implementation, and code generation techniques, are briefly reviewed.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence