Trustworthy Systems

An empirical research agenda for understanding formal methods productivity

Authors

Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein and Toby Murray

NICTA

UNSW

Abstract

Formal methods, and particularly formal verification, is becoming more feasible to use in the engineering of large highly dependable software-based systems, but so far has had little rigorous empirical study. Its artefacts and activities are different to those of conventional software engineering, and the nature and drivers of productivity for formal methods are not yet understood.

To develop a research agenda for the empirical study of productivity in software projects using formal methods and in particular formal verification. To this end we aim to identify research questions about productivity in formal methods, and survey existing literature on these questions to establish face validity of these questions. And further we aim to identify metrics and data sources relevant to these questions.

We define a space of GQM goals as an investigative framework, focusing on productivity from the perspective of managers of projects using formal methods. We then derive questions for these goals using Easterbrook et al.’s (2008) taxonomy of research questions. To establish face validity, we document the literature to date that reflects on these questions and then explore possible metrics related to these questions. Extensive use is made of literature concerning the L4.verified project completed within NICTA, as it is one of the few projects to achieve code-level formal verification for a large-scale industrially deployed software system.

We identify more than thirty research questions on the topic in need of investigation. These questions arise not just out of the new type of project context, but also because of the different artefacts and activities in formal methods projects. Prior literature supports the need for research on the questions in our catalogue, but as yet provides little evidence about them. Metrics are identified that would be needed to investigate the questions. Thus although it is obvious that at the highest level concepts such as size, effort, rework and so on are common to all software projects, in the case of formal methods, measurement at the micro level for these concepts will exhibit significant differences.

Empirical software engineering for formal methods is a large open research field. For the empirical software engineering community our paper provides a view into the entities and research questions in this domain. For the formal methods community we identify some of the benefits that empirical studies could bring to the effective management of large formal methods projects, and list some basic metrics and data sources that could support empirical studies. Understanding productivity is important in its own right for efficient software engineering practice, but can also support future research on cost-effectiveness of formal methods, and on the emerging field of Proof Engineering.

BibTeX Entry

  @article{Jeffery_SAKM_15,
    author           = {Jeffery, Ross and Staples, Mark and Andronick, June and Klein, Gerwin and Murray, Toby},
    journal          = {Information and Software Technology},
    keywords         = {empirical software engineering; productivity; gqm; formal methods; formal verification; proof
                        engineering},
    month            = jan,
    pages            = {102--112},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8312.pdf},
    title            = {An Empirical Research Agenda for Understanding Formal Methods Productivity},
    volume           = {60},
    year             = {2015}
  }

Download