Advanced software specification and verification

Abstract

In today’s “Information Society” more and more tasks are performed automatically or semi-automatically by software products. Moreover, some of these tasks have critical security requirements (e.g., is it possible to ensure that the transactions between client and server will always be private; the process will always terminate, etc.). In this context, it is crucial to incorporate processes that ensure that the developed software meets a number of requirements. For this purpose, it is possible to use experimental methods based on testing (which usually cannot assure 100% that the requirements are fulfilled) or formal verification methods based on the use of models, the incorporation of assertions in the code, etc. In this second case, it is possible to obtain a total guarantee of the correctness of the software. In our group, we focus on the use of models based on “Petri nets” for the formal specification of certain processes (in particular, they are particularly suitable for formalizing tasks involving concurrency, inter-process communication, synchronization, etc.). The main advantage of using such formal models is that there are a number of software tools that allow their analysis and verification in a semi-automatic way. Another technology used in the group is based on the use of JML (Java Modelling Language), a language for the definition of assertions that are incorporated in Java programs and allow testing different properties of them (either at runtime or statically). For example, JML can be used to include assertions about safety conditions in critical software, so that if the conditions are violated, code execution is aborted.

Scientific officer

Oliver Villarroya Francisco Javier

Stakeholders

Applications

  • Formal specification techniques make it possible to detect errors in the initial phases of software development, thus considerably reducing the high cost of eliminating errors in the exploitation phase.
  • On the other hand, verification techniques based on JML can significantly contribute to improve software quality and to certify, in some cases, that the software meets certain requirements regarding its performance, security, etc.

Technical advantages

Formal techniques have a number of unquestionable advantages over more traditional techniques based on testing and experimentation, since they make it possible to “certify” (in some cases with 100% reliability) that the software developed complies with a series of requirements (security, termination, etc.).

Benefits it provides

  • More reliable and certified software
  • Many of the techniques mentioned have a very low implementation cost (for example, the inclusion of JML assertions in Java applications can be easily done by the programmers themselves).

Relevant experience

Since its creation, the group has been oriented to the development of techniques related to the topics discussed here, which is supported by the number and quality of the publications of the team members, as well as by the R+D+i projects in which we have participated.