Formal Specification of Scientific Applications Using Interval Temporal Logic

Abstract

Scientific applications simulate any natural phenomena in different scientific domains. Moreover, the problems they solve are usually represented by mathematical models. Taking that in advance, these problems can be described by using specific formal notation and mathematical formulas. Scientific applications are usually created by the scientists without using any software development engineering practices. Our main goal is to include formal methods in the testing process of scientific applications. In this paper, we adapt Interval Temporal Logic (ITL) as a flexible notation for describing software applications. We use Tempura framework and Ana Tempura tool for specifying the properties of the scientific software system. The correctness of the code is verified by comparing the results from the program output and functions written in Tempura. This process is especially important when some code changes or optimizations are made. To verify this concept we made a formal description of the code for calculating bound states of the Morse oscillator well.