Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code.

Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code

Studies on Thermodynamics and No-hair Theorem in Black hole Spacetime

Department of Physics, Cochin University of Science and Technology

Enhancement of Microwave Properties of Planar Filters and Antennas using Photonic Bandgap (PBG) Structures

In this thesis, we explore the design, computation, and experimental analysis of photonic crystals, with a special emphasis on structures and devices that make a connection with practically realizable systems. First, we analyze the propenies of photonic-crystal: periodic dielectric structures that have a band gap for propagation. The band gap of periodically loaded air column on a dielectric substrate is computed using Eigen solvers in a plane wave basis. Then this idea is extended to planar filters and antennas at microwave regime. The main objectives covered in this thesis are:• Computation of Band Gap origin in Photonic crystal with the abet of Maxwell's equation and Bloch-Floquet's theorem • Extension of Band Gap to Planar structures at microwave regime • Predict the dielectric constant - synthesized dieletric cmstant of the substrates when loaded with Photonic Band Gap (PBG) structures in a microstrip transmission line • Identify the resonant characteristic of the PBG cell and extract the equivalent circuit based on PBG cell and substrate parameters for microstrip transmission line • Miniaturize PBG as Defected Ground Structures (DGS) and use the property to be implemented in planar filters with microstrip transmission line • Extended the band stop effect of PBG / DGS to coplanar waveguide and asymmetric coplanar waveguide. • Formulate design equations for the PBG / DGS filters • Use these PBG / DGS ground plane as ground plane of microstrip antennas • Analysis of filters and antennas using FDID method

Topological Invariants in Hydrodynamics and Hydromagnetics

In this thesis we are studying possible invariants in hydrodynamics and hydromagnetics. The concept of flux preservation and line preservation of vector fields, especially vorticity vector fields, have been studied from the very beginning of the study of fluid mechanics by Helmholtz and others. In ideal magnetohydrodynamic flows the magnetic fields satisfy the same conservation laws as that of vorticity field in ideal hydrodynamic flows. Apart from these there are many other fields also in ideal hydrodynamic and magnetohydrodynamic flows which preserves flux across a surface or whose vector lines are preserved. A general study using this analogy had not been made for a long time. Moreover there are other physical quantities which are also invariant under the flow, such as Ertel invariant. Using the calculus of differential forms Tur and Yanovsky classified the possible invariants in hydrodynamics. This mathematical abstraction of physical quantities to topological objects is needed for an elegant and complete analysis of invariants.Many authors used a four dimensional space-time manifold for analysing fluid flows. We have also used such a space-time manifold in obtaining invariants in the usual three dimensional flows.In chapter one we have discussed the invariants related to vorticity field using vorticity field two form w2 in E4. Corresponding to the invariance of four form w2 ^ w2 we have got the invariance of the quantity E. w. We have shown that in an isentropic flow this quantity is an invariant over an arbitrary volume.In chapter three we have extended this method to any divergence-free frozen-in field. In a four dimensional space-time manifold we have defined a closed differential two form and its potential one from corresponding to such a frozen-in field. Using this potential one form w1 , it is possible to define the forms dw1 , w1 ^ dw1 and dw1 ^ dw1 . Corresponding to the invariance of the four form we have got an additional invariant in the usual hydrodynamic flows, which can not be obtained by considering three dimensional space.In chapter four we have classified the possible integral invariants associated with the physical quantities which can be expressed using one form or two form in a three dimensional flow. After deriving some general results which hold for an arbitrary dimensional manifold we have illustrated them in the context of flows in three dimensional Euclidean space JR3. If the Lie derivative of a differential p-form w is not vanishing,then the surface integral of w over all p-surfaces need not be constant of flow. Even then there exist some special p-surfaces over which the integral is a constant of motion, if the Lie derivative of w satisfies certain conditions. Such surfaces can be utilised for investigating the qualitative properties of a flow in the absence of invariance over all p-surfaces. We have also discussed the conditions for line preservation and surface preservation of vector fields. We see that the surface preservation need not imply the line preservation. We have given some examples which illustrate the above results. The study given in this thesis is a continuation of that started by Vedan et.el. As mentioned earlier, they have used a four dimensional space-time manifold to obtain invariants of flow from variational formulation and application of Noether's theorem. This was from the point of view of hydrodynamic stability studies using Arnold's method. The use of a four dimensional manifold has great significance in the study of knots and links. In the context of hydrodynamics, helicity is a measure of knottedness of vortex lines. We are interested in the use of differential forms in E4 in the study of vortex knots and links. The knowledge of surface invariants given in chapter 4 may also be utilised for the analysis of vortex and magnetic reconnections.

Theory of differential inequalities with appliciations to singular perturbiation problems and method of lines

During recent years, the theory of differential inequalities has been extensively used to discuss singular perturbation problems and method of lines to partial differential equations. The present thesis deals with some differential inequality theorems and their applications to singularly perturbed initial value problems, boundary value problems for ordinary differential equations in Banach space and initial boundary value problems for parabolic differential equations. The method of lines to parabolic and elliptic differential equations are also dealt The thesis is organised into nine chapters