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.
- Visual formalisms
- State-transition diagrams
- Software specification
- Formal Methods
Gülesir, G., Bergmans, L., Aksit, M., & van den Berg, K. (2013). Vibes: a visual language for specifying behavioral requirements of algorithms. Journal of visual languages and computing, 24(5), 350-364. https://doi.org/10.1016/j.jvlc.2013.08.005