Vibes: a visual language for specifying behavioral requirements of algorithms

G. Gülesir, Lodewijk Bergmans, Mehmet Aksit, Klaas van den Berg

    Research output: Contribution to journalArticleAcademicpeer-review

    3 Citations (Scopus)

    Abstract

    Manually verifying the behavior of software systems with respect to a set of requirements is a time-consuming and error-prone task. If the verification is automatically performed by a model checker however, time can be saved, and errors can be prevented. To be able to use a model checker, requirements need to be specified using a formal language. Although temporal logic languages are frequently used for this purpose, they are neither commonly considered to have sufficient usability, nor always naturally suited for specifying behavioral requirements of algorithms. Such requirements can be naturally specified as regular language recognizers such as deterministic finite accepters, which however suffer from poor evolvability: the necessity to re-compute the recognizer whenever the alphabet of the underlying model changes. In this paper, we present the visual language Vibes that both is naturally suited for specifying behavioral requirements of algorithms, and enables the creation of highly evolvable specifications. Based on our observations from controlled experiments with 23 professional software engineers and 21 M.Sc. computer science students, we evaluate the usability of Vibes in terms of its understandability, learnability, and operability. This evaluation suggests that Vibes is an easy-to-use language.
    Original languageUndefined
    Pages (from-to)350-364
    Number of pages15
    JournalJournal of visual languages and computing
    Volume24
    Issue number5
    DOIs
    Publication statusPublished - Oct 2013

    Keywords

    • Visual formalisms
    • State-transition diagrams
    • Software specification
    • Formal Methods
    • METIS-300007
    • IR-87446
    • EWI-23685

    Cite this

    Gülesir, G. ; Bergmans, Lodewijk ; Aksit, Mehmet ; van den Berg, Klaas. / Vibes: a visual language for specifying behavioral requirements of algorithms. In: Journal of visual languages and computing. 2013 ; Vol. 24, No. 5. pp. 350-364.
    @article{0451fb5c611c4fe9837cde2ed49fc29f,
    title = "Vibes: a visual language for specifying behavioral requirements of algorithms",
    abstract = "Manually verifying the behavior of software systems with respect to a set of requirements is a time-consuming and error-prone task. If the verification is automatically performed by a model checker however, time can be saved, and errors can be prevented. To be able to use a model checker, requirements need to be specified using a formal language. Although temporal logic languages are frequently used for this purpose, they are neither commonly considered to have sufficient usability, nor always naturally suited for specifying behavioral requirements of algorithms. Such requirements can be naturally specified as regular language recognizers such as deterministic finite accepters, which however suffer from poor evolvability: the necessity to re-compute the recognizer whenever the alphabet of the underlying model changes. In this paper, we present the visual language Vibes that both is naturally suited for specifying behavioral requirements of algorithms, and enables the creation of highly evolvable specifications. Based on our observations from controlled experiments with 23 professional software engineers and 21 M.Sc. computer science students, we evaluate the usability of Vibes in terms of its understandability, learnability, and operability. This evaluation suggests that Vibes is an easy-to-use language.",
    keywords = "Visual formalisms, State-transition diagrams, Software specification, Formal Methods, METIS-300007, IR-87446, EWI-23685",
    author = "G. G{\"u}lesir and Lodewijk Bergmans and Mehmet Aksit and {van den Berg}, Klaas",
    note = "eemcs-eprint-23685",
    year = "2013",
    month = "10",
    doi = "10.1016/j.jvlc.2013.08.005",
    language = "Undefined",
    volume = "24",
    pages = "350--364",
    journal = "Journal of visual languages and computing",
    issn = "1045-926X",
    publisher = "Academic Press Inc.",
    number = "5",

    }

    Vibes: a visual language for specifying behavioral requirements of algorithms. / Gülesir, G.; Bergmans, Lodewijk; Aksit, Mehmet; van den Berg, Klaas.

    In: Journal of visual languages and computing, Vol. 24, No. 5, 10.2013, p. 350-364.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Vibes: a visual language for specifying behavioral requirements of algorithms

    AU - Gülesir, G.

    AU - Bergmans, Lodewijk

    AU - Aksit, Mehmet

    AU - van den Berg, Klaas

    N1 - eemcs-eprint-23685

    PY - 2013/10

    Y1 - 2013/10

    N2 - Manually verifying the behavior of software systems with respect to a set of requirements is a time-consuming and error-prone task. If the verification is automatically performed by a model checker however, time can be saved, and errors can be prevented. To be able to use a model checker, requirements need to be specified using a formal language. Although temporal logic languages are frequently used for this purpose, they are neither commonly considered to have sufficient usability, nor always naturally suited for specifying behavioral requirements of algorithms. Such requirements can be naturally specified as regular language recognizers such as deterministic finite accepters, which however suffer from poor evolvability: the necessity to re-compute the recognizer whenever the alphabet of the underlying model changes. In this paper, we present the visual language Vibes that both is naturally suited for specifying behavioral requirements of algorithms, and enables the creation of highly evolvable specifications. Based on our observations from controlled experiments with 23 professional software engineers and 21 M.Sc. computer science students, we evaluate the usability of Vibes in terms of its understandability, learnability, and operability. This evaluation suggests that Vibes is an easy-to-use language.

    AB - Manually verifying the behavior of software systems with respect to a set of requirements is a time-consuming and error-prone task. If the verification is automatically performed by a model checker however, time can be saved, and errors can be prevented. To be able to use a model checker, requirements need to be specified using a formal language. Although temporal logic languages are frequently used for this purpose, they are neither commonly considered to have sufficient usability, nor always naturally suited for specifying behavioral requirements of algorithms. Such requirements can be naturally specified as regular language recognizers such as deterministic finite accepters, which however suffer from poor evolvability: the necessity to re-compute the recognizer whenever the alphabet of the underlying model changes. In this paper, we present the visual language Vibes that both is naturally suited for specifying behavioral requirements of algorithms, and enables the creation of highly evolvable specifications. Based on our observations from controlled experiments with 23 professional software engineers and 21 M.Sc. computer science students, we evaluate the usability of Vibes in terms of its understandability, learnability, and operability. This evaluation suggests that Vibes is an easy-to-use language.

    KW - Visual formalisms

    KW - State-transition diagrams

    KW - Software specification

    KW - Formal Methods

    KW - METIS-300007

    KW - IR-87446

    KW - EWI-23685

    U2 - 10.1016/j.jvlc.2013.08.005

    DO - 10.1016/j.jvlc.2013.08.005

    M3 - Article

    VL - 24

    SP - 350

    EP - 364

    JO - Journal of visual languages and computing

    JF - Journal of visual languages and computing

    SN - 1045-926X

    IS - 5

    ER -