FormulaBuilder: A tool for graph-based modelling and generation of formulae

Sven Jörges, Tiziana Margaria, Bernhard Steffen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

In this paper we present the FormulaBuilder, a flexible tool for graph-based modelling and generation of formulae. The FormulaBuilder allows easy and intuitive creation of formulae by using basic components called Formula Building Blocks (FBBs) and arranging them as graphs according to the syntactic structure of a formula. Such a graph can then be validated and used to generate the corresponding formula on the basis of a specific syntax which is chosen from a list of syntaxes supported by the FormulaBuilder. An important application of the FormulaBuilder is the formal specification of properties that describe the requirements of a system. Such property specifications are usually needed by verification tools like model checkers, that help software engineers to detect errors in a specified system. The FormulaBuilder allows users to model property specifications as formula graphs by using commonly-occurring specification patterns.

Original languageEnglish
Title of host publicationProceeding of the 28th International Conference on Software Engineering 2006, ICSE '06
Pages815-818
Number of pages4
Publication statusPublished - 2006
Externally publishedYes
Event28th International Conference on Software Engineering 2006, ICSE '06 - Shanghai, China
Duration: 20 May 200628 May 2006

Publication series

NameProceedings - International Conference on Software Engineering
Volume2006
ISSN (Print)0270-5257

Conference

Conference28th International Conference on Software Engineering 2006, ICSE '06
Country/TerritoryChina
CityShanghai
Period20/05/0628/05/06

Keywords

  • Formula generation
  • Property specification
  • Specification patterns

Fingerprint

Dive into the research topics of 'FormulaBuilder: A tool for graph-based modelling and generation of formulae'. Together they form a unique fingerprint.

Cite this