Formal Specification of Scientific Applications Using Interval Temporal Logic
Date Issued
2014
Author(s)
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.
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.
File(s)![Thumbnail Image]()
Loading...
Name
SQAMIA2014_Paper5.pdf
Size
243.26 KB
Format
Adobe PDF
Checksum
(MD5):3acd70284fa03c88e8b817c635811ec0