Scienti c applications simulate any natural phenomena in di erent scienti c domains. Moreover, the problems they solve are usually represented by mathematical models. Taking that in advance, these problems can be described by using speci c formal notation and mathematical formulas. Scienti c 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 scienti c applications. In this paper, we adapt Interval Temporal Logic (ITL) as a exible notation for describing software applications. We use Tempura framework and Ana Tempura tool for specifying the properties of the scienti c software system. The correctness of the code is veri ed 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.
5:30 into three categories: complexity of the theory and the difficulty of its validation; implementation risks (code and documentation) and application usage risk (concerning the use of the application by the target user groups). Validation is difficult because the results sometimes must be compared with the results obtained by the physical experiments. Also, scientists usually visually decide whether the results are satisfactory or not. The survey presented in [Koteska and Mishev 2013] shows that most of the interviewed scientists do not prefer formal software engineering testing methods, do not use any testing tools, do not use any specific test case generation technique and some of them do ad-Hoc testing.
To change the current development practices and to improve testing, we propose adapting the method of formal specification and verification of the scientific applications. We chose Interval Temporal Logic (ITL) as a powerful and flexible mathematical notation for propositional and First-order reasoning about periods of time which is used for describing hardware and software systems. We also use the Ana Tempura tool that is built upon C-Tempura and is used for runtime verification of systems. This tool uses ITL and the executable subset Tempura which is an interpreter for executable ITL formulas [Cau et al. 2002]. As a case study, we chose the code for calculating the bound states of the Morse oscillator well which is described in [Bittner 2009].
The rest of the paper is organized as follows. Related work is given in Section 2. In Section 3, we explain the importance of using the formal notation for scientific application description and we present the benefits of using ITL and Tempura. In Section 4, the ITL formal description of the code for calculating the bound states of the Morse oscillator well is given and the results of the testing process are shown. The conclusion and future work are specified in Section 5.
There are several research papers that present some methods for formal description of software systems and architectures. An overview of how formal (mathematical) methods can be used in the software development cycle and what methods and tools can support software development is given in [Ostroff and Paige 1998]. Siegel and Avrunin [Siegel and Avrunin 2004] write about issues related to finitestate verification techniques when applied to scientific computation software employing the Open MPI (open source High Performance Message Passing Interface implementation). Siegel and Rossi [Siegel and Rossi 2008] applied model checking techniques to BlobFlow (MPI scientific program consisted of 10K lines of code that implements a high order vortex method for solving the two-dimensional NavierStokes equations).ITL has been previously used for describing software or hardware systems, state machines or documents. For example, Sciavicco et al. [Sciavicco et al. 2009] consider the problem of formalizing a medical guideline in a logical language. These guidelines are documents supporting the health-care professionals in managing a disease in a patient. Zedan et al. [Zedan et al. 1999] present an object based formal method for the development of real-time systems which is called ATOM. It is based on the refinement calculus and also the formal specification contains ITL description of the behaviour of a real-time system. El-kustaban et al. [El-kustaban et al. 2012] proposed an executable specification model for an abstract transactional memory (lock-free technique that offers a parallel programming model for future chip multiprocessor systems). They used ITL and AnaTempura to build and validate the model. In [Rossi et al. 2004], the authors use temporal logic that combines points, intervals, and dates to formalize the semantics of UML state machines.
The development of scientific applications does not include software engineering practices or formal methods which means that no requirements, formal specification or any kind of documentation could be found. The problems come later when some code modifications or optimization should be performed and nobody knows what the code function is. ITL is usually used for modeling critical software systems, but it really helps when some code changes are made. For example, code changes must be made when some code optimizations are performed which happens very usually while programming scientific applications because of the memory lack and CPU performance. The program written in Tempura is one way to check the correctness of the results of the program. It also helps for understanding the order of the statements execution at a given moment of time. If no formal program description is used, then the chances for program errors are bigger and the program is less understandable for people being included in the development process later.
The research shows that no formal specification of the scientific applications using ITL/ Tempura are made. Our main goal is to give a formal code description in order to change the current practices, to give a mathematical representation of the scientific problem and to improve the process of verification.
This section presents the benefits of making formal description and verification of scientific applications by using Interval Temporal Logic and Tempura.
Some of the most important benefits of using formal methods are given below [Hall 2005; Groote et al. ; Sommerville 2007; Woodcock et al. 2009; van der Poll 2010; Jaeger 2010; Clarke and Wing 1996]: —The formal software description is abstract and precise description which means that a human reader can understand the big picture and all ambiguities can be removed. —Formal description allows users to make rigorous analysis and to determine useful properties such as consistency or deadlock-freedom. —Using formal methods when developing complex software results in higher quality, more correct software, and discovering errors that may not have been discovered through traditional testing. —Formal specification allows users to find the problems and ambiguities in the system requirements. —Formal methods are used for code verification which is attempt to prove the theorem that if certain condition are satisfied the program will achieve the expected results. —Formal methods facilitate the production of quality and testing. Maintenance phases are shortened. —The use of formal methods increases the development correctness confidence and has the potential to eliminate some types of errors in the system. —Formal methods can increase the understanding of the system by removing inconsistencies, ambiguities and incompleteness.
Formal methods are usually applied to the critical systems development, but there are also critical scientific applications, especially in the bioinformatics research field. These applications have critical implications for life sciences and require strong quality assurance [Umarji et al. 2009].
Interval Temporal Logic (ITL) is a formalism that is an extension to standard predicate logic which includes time-dependent operators [Moszkowski and Manna 1984]. The key term of ITL is an interval. An interval is defined as a (in)finite sequence of states where each state is a mapping from the set of variables to the set of values [Cau et al. 2002].
Expression in ITL is defined as: exp ::= z j a j A j g(exp1; :::; expn) j {a : f , where z is an integer value, a is a static variable (its value cannot be changed within an interval), A is a state variable (its value can be changed within an interval), g is a function symbol, f is a formula.
Formula in ITL is defined as: f ::= p(exp1; :::; expn) j :f j f1 ^ f2 j 8v f j skip j f1; f2 j f , where p is a predicate symbol, ; is a chop symbol.
Formulas are building inductively as follows: —Equality: exp1 = exp2
f —Always: f —Logical connectives: :f and f1 ^ f2 —Next:
The informal semantics can be represented as follows: —{a : f - choose value of a such that f holds —skip - interval with length 1 —f1; f2 - the interval is decomposed into two intervals (prefix interval such that f1 holds and suffix interval such that f2 holds) or the interval is infinite and f1 holds. —f - the interval is decomposable into a finite number of intervals such that for each of them f holds, or the interval is infinite and it can be decomposed into an infinite number of intervals such that f holds [?].
For example, this is a valid ITL formula: (I = 2) ^ (K = 3). It can be interpreted as follows: in the current state I is 2 and in the next state K will be 3.
Interval Temporal Logic provides a basis for the programming language Tempura. The main syntactic categories in Tempura are: expressions (can be boolean or arithmetic), statements (temporal formulas that can be simple or compound) and locations (places where values are stored) [Moszkowski 1985]. A formula is executable in tempura if the following three characteristics are satisfied: the formula is deterministic, the length of an interval is known and the values of the variables are known through that interval [De Montfort University 2004].
In this section, we refer to the problem of finding the bound states of Morse oscillator (i.e. solving the stationary Schro¨dinger equation for Morse potential) and we present the formal specification of the code by using ITL and Ana Tempura. The Morse oscillator well have not been modeled yet with ITL and Tempura. The reason that we chose it for modeling is that code is simple to be understand and it also can be considered as an example of a simple scientific application.
Calculation of eigenenergies of bound states of Morse oscillator is a prototypical exercise in quantum mechanics. This is so since the particular potential serves as a model system for studying molecular vibrations. Morse potential has the following form:
U (r) = De [1 exp( (r re))]2 (1) where De denotes the dissociation energy of the corresponding bond, while re is the interatomic distance corresponding to the minimum energy of the oscillator. Vibrational Schro¨dinger equation with the potential of the form (1) is analytically solvable and the corresponding vibrational eigenenergies are given by: Ev = h c [(v + 1 ) !e (v + 1 )2 !exe] (2)
2 2
In eq. (2), v is the vibrational quantum number (v 2 0; 1; 2; ), !exe is the so-called anharmonicity constant and is related to the parameter and the reduced mass of the oscillator by: = 2 c !e r
All other symbols in (2) have their usual meanings. The fact that the vibrational Scho¨dinger equation for Morse oscillator is analytically solvable makes this system a rather convenient test case for a number of numerical methods aimed to solve the quantum vibrational problem.
In our particular application of the formal code specification approach, we solve the vibrational eigenvalue problem by the discrete variable representation methodology [J. C. Light and J. V. Lill 1985], following closely the approach adopted by Bittner [Bittner 2009]. To solve a problem in quantum mechanics by using numerical methods, the Hamiltonian operator should be represented in a finite polynomial basis. In this case, the Tchebychev polynomials are used as a basis.
One of the methods we made a formal specification for is thcheby(...). It returns a set of points pts[NPTS], the eigenstates the Laplacian operator, ( 2@=@x2), in the basis ke f b[NPTS] (kinetic energy in finite basis), set of weights w[NPTS] and a transformation matrix T [NPTS][NPTS]. NPTS is the number of points. There are two representations: finite basis representation (FBR) and discrete variable representation (DVR). The transformation matrix carries one from the FBR to a DVR. double thcheby(double xmin, double xmax, double pts[],double ke_fb[], double w[],double T[][NPTS]) { double del, fb; int i,j; del=xmax-xmin; for(i=0;i<NPTS;i++) { pts[i]=((i+1)*del)/(NPTS+1)+xmin; ke_fb[i]=square((i+1)*M_PI/del); w[i]=del/(NPTS+1); for(j=0;j<NPTS;j++) { } } }
T[i][j]= sqrt(2.0/(NPTS+1))*sin(((i+1)*(j+1)*M_PI)/(NPTS+1));
To solve the bound states of the Morse oscillator well we should define the number of points: NPTS= 100, and range: xmin = 3 and xmax = 32. The goal is to construct the Hamiltonian matrix in the DVR basis and then diagonalize it to determine the eigenvalues and eigenvectors. The eigenvalues (energies) below 0 are bound states. We use the eigenvectors and eigenvalues to plot the wave functions. We automated the part for checking the correctness of wavefunctions by checking the values of the first two eigenvectors. A wave function is correct if the difference between two neighbor values is smaller than 10 3 and the values gradually getting tend to zero.
1V -1 -2 -3 5 10 15 20 25 30 x
Wave functions
We made a formal specification of the code for calculating the bound states of the Morse oscillator well by writing a Tempura code and making tests to compare the output results from the .exe version of the C program and Tempura code. In order to establish communication between the tempura file and the .exe version of the C program assertions must be added in the C code. We will explain the C and Tempura code where the checking of the values in the ke fb[] array is performed. The code for checking the other arrays and values is similar. int i=0; double ke_fb_i=0.00000; assertion1 ("ke_fb_i", ke_fb_i); assertion ("i", i); while (i<NPTS) { ke_fb_i=square((i+1)*M_PI/del); assertion1 ("ke_fb_i", ke_fb_i); i=i+1;assertion ("i", i); }
The assertion functions are used for checking the values of the variables after each performed change. The values of the variables are compared to the values obtained from the Tempura code.
Here is the function for calculating the Y -th value of the ke fb[] array written in Tempura language. The function itof returns the float corresponding to an integer number and del = xmax xmin. define calc_ke_fb(Y) = {
if Y>=0 then {((itof(Y)+$1.0$)*M_PI/del)*((itof(Y)+$1.0$)*M_PI/del) } else empty }.
Here is the test we defined to check the results: /* run */ define test1() = { exists ke_fb_i, Y :
The function check compare the results from the calc ke fb function and the C program. If they are identical, test passed. The results from the first two iterations when a test is run by the Ana Tempura tool are shown in 2. These test cases pass successfully.
In this paper we presented the importance of using formal methods for testing and specification of scientific software. A formal specification of the code for solving the bound states of the Morse oscillator well by using ITL and Ana Tempura was described. Also the implementation details and steps were given. Formal specification and description of the scientific software will improve its correctness by reducing the number of errors, especially when a code change is made. The testing also will be more accurate and mathematical model will be provided for the software. We chose ITL and Tempura as a powerful description language and extension to standard predicate logic which includes time-dependent operators. The programs written in Tempura and executed in Ana Tempura tool can communicate with .exe version of the programs. At this moment, there are examples of program codes 5:36 written in C and Java. There are no limitations of the number of test cases that can be covered. Tempura language is similar to predicate logic and it is easy to be learned. There are only several rules and categories such as expressions, statements and locations. The hard part for the scientists could be the programming with recursion.
We plan to make a formal specification of the scientific application which is developed within the HP-SEE (High-Performance Computing Infrastructure for South East Europe) project. We want to automate the testing process by creating and running tests using the Ana Tempura tool.