Addressing usability in a formal development environment

Abstract

Even though the formal method community tends to overlook the problem, formal methods are sometimes difficult to use and not accessible to average users. On one hand, this is due to the intrinsic complexity of the methods and, therefore, some level of required expertise is unavoidable. On the other hand, however, the methods are sometimes hard to use because of lack of a user-friendly tool support. In this paper, we present our experience in addressing usability when developing a framework for the Abstract State Machines (ASMs) formal method. In particular, we discuss how we enhanced modeling, validation, and verification activities of an ASM-based development process. We also provide a critical review of which of our efforts have been more successful as well as those that have not obtained the results we were expecting. Finally, we outline other directions that we believe could further lower the adoption barrier of the method.