Vibes: A visual language for specifying behavioral requirements of algorithms

• Vibes is a visual language for specifying behavioral requirements of algorithms.
• Vibes is easy to use and enables creation of highly evolvable specifications.
• Vibes combines strengths and eliminates weaknesses of temporal logics and DFAs.
• Expressive power of Vibes defines open regular languages, which is a new family of formal languages.
• The set of open regular languages partially lie outside Chomsky Hierarchy.

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.