Analysing memory and time consumption properties of Java programs with ResAna

Spreker: Marko van Eekelen.

Abstract

In the areas of technical and civil engineering there is a long tradition in which developers employ dedicated tools that analyse and verify technical designs. Such tools are based on formal properties of the models involved. Such properties are often quality properties such as strength, safety and stability. In many cases the tool indicates that the design satisfies a certain upper bound or a lower bound of the property.

In the area of software engineering the use of formal method based tools is present mainly in the academic world, and only occasionally in every day development. Furthermore, the largest amount of effort in the use of such tools is geared towards functional verification, i.e. whether the software fulfills the right functionality producing the right output upon receiving certain inputs. Quality characteristics such as time and space complexity are often restricted to some measurements on running software.

In the context of the EU-CHARTER project which aims at producing software development tool for safety critical application areas (such as automotive,aerospace, surveillance and healthcare), researchers from the University of Nijmegen have developed a prototype tool (ResAna) to analyse time and space complexity properties of Java programs. Time and space are considered to be resources that are consumed by the program and the tool ResAna performs resource consumption analysis based on formal methods.

ResAna can analyse loop bounds, heap bounds and stack bounds. It is open source, can be used as a plugin in the Eclipse IDE and it interacts with other CHARTER developed tools to deliver its results. ResAna has been used in case studies by the industrial partners of the CHARTER project to analyse the complexity of their programs.

The talk will report both on the underlying formal analysis methods of the tool and on its practical applicability, by showing some key examples of its use.

Biography

Prof.dr. Marko van Eekelen studied mathematics in Nijmegen. Under the supervision of Prof. Barendregt he obtained his PhD. in 1988 in Nijmegen. In 2004 he became a member of the Digital Security group of the Radboud Universiteit Nijmegen. Since early this year, he is also appointed to the Software Technology Chair of the Open Universiteit Nederland.

He is the scientific director of the Nijmegen section of LaQuSo (Laboratory for Quality Software), a joint activity of TU Eindhoven and Radboud Universiteit Nijmegen in which quality assessments are performed for industrial software products.

For several years now, he is actively involved in research in software analysis of non-functional properties such as resource consumption and security and privacy.

See also his personal webpage.