Parameter identifiability is an important aspect of parameter estimation of dynamic system modelling. Several methods exist to determine identifiability of parameter sets using the model definition and analysis of experimental data. There is also the possibility of some parameters being independently unidentifiable but forming identifiable parameter combinations. These identifiable parameter combinations are useful in model reparameterisation to estimate parameters experimentally. Multiple numerical and algebraic methods exist to detect identifiable parameter combinations of dynamic system models represented as ordinary differential equations (ODE). Local identifiability analysis of hybrid system models are available in the literature. However, methods for structural identifiability analysis and identifiable combination detection for hybrid systems are not explored. Here, we have developed a parameter identifiable combination detection method for non-linear hybrid systems along with ODE systems using an SMT based parameter space exploration method. For higher dimensional systems and larger parameter space, SMT based approaches may easily become computationally intractable. This problem has been mitigated to a large extent by heuristically limiting the parameter space to be explored, using Gaussian process regression and gradient based approaches. The developed method has been demonstrated for some simple hybrid models, biochemical models of ODE systems and non-linear hybrid systems.

In recent times, Bounded Model Checking (BMC) engines have gained wide prominence in formal verification. Different BMC engines exist, differing in their optimization, representations and solving mechanisms used to represent and navigate the underlying state transition of the given design to be verified. The objective of this article is to examine if combinations of BMC engines can help to combine their strengths. We propose an approach that can create a sequencing of BMC engines that can reach better depth in formal verification, as opposed to executing them alone for a specified time. Our approach uses machine learning, specifically, the Multi-Armed Bandit paradigm of reinforcement learning, to predict the best-performing BMC engine for a given unrolling depth of the underlying circuit design. We evaluate our approach on a set of benchmark designs from the Hardware Model Checking Competition (HWMCC) benchmarks and show that it outperforms the state-of-the-art BMC engines in terms of the depth reached or time taken to deduce a property violation. The synthesized BMC engine sequences reach better depths than HWMCC results and the state-of-the-art technique, super_deep, for more than 80% of the cases. It also outperforms single engine runs for more than 92% of the cases where a property violation is not found within a given time duration. For designs where property violations are found within the given time duration, the synthesized sequences found the property violation in a lesser time than HWMCC for all the designs and outperformed both super_deep and single engine runs for more than 87% of the designs.

An ordinary differential equation (ODE) model of the working of the thyroid system for euthyroidism has been presented. As clinical data for thyroid hormones is relatively scarce, such modelling offers potential benefits over wet lab procedures. Genetic algorithms developed for determining of parameters of the ODE system using the available data have been presented and evaluated. This approach enables subject specific parameter estimation towards characterisation of individual thyroid operation. Initially, a simple steady state model was used. Later a cosinor model for the circadian variation of thyroid hormones was used to obtain more reliable results, as indicated through sensitivity analysis in conjunction with other statistical methods. Our parameter determination method has been tested on groups of patients with similar observed values of thyroid stimulating hormone (TSH), free T$_3$3and free T$_4$4(identified through clustering) to determine their parameter values jointly. This approach appears to produce parameter sets with lower variation than parameters determined independently, thus leading to better parameter determination.

Railway signalling is a complex and safety critical problem that has been extensively studied and standardised over a long period of time. The signalling equipment is typically procured from standard vendors and configured with yard specific application logic for which the route control chart (RCC) is a key input. As the yard size increases, the number of routes also increases and accordingly the difficulty of RCC preparation increases rapidly. RCC preparation for big yards may take months and affects the project deadlines adversely. In this work we report computational procedures to address:$a$) capturing of signal interlocking plan (SIP) given on paper and storing it using suitable data structures,$b$) generating the RCC automatically from the captured SIP supported by procedures based on graph theoretic formulation,$c$) storing the SIP graphically in memory,$d$) application of formal methods towards validation of yard structure and$e$) generation of temporal logic properties for formal verification of electronic interlocking (EI) logic. Several important steps towards RCC generation, such as conflict identification and isolation determination and also validation and verification (V&V) covering yard layout and safety property generation based on graph theoretic modelling are the most interesting aspect of this work. The described techniques have been tested successfully on many actual yards.

In railway electronic interlocking system, the automatic signalling equipment is programmed with the configuration data derived manually from the yard layout. This step is prone to human errors and any error can be a severe threat to signalling safety. The yard-layout data and the configured system both need to be verified to satisfy the desired safety requirements. The configured signalling system is needed to be verified against those relevant safety properties before deploying. Accordingly, the contributions in this paper include, (a) validation of input in terms of yard-layout data against some spatial properties (b) generation of yard-specific properties from the validated layout data for interlocking system verification. The work described in this paper is applied for signalling rules followed by Indian Railways. To capture the actual environment, a set of complex properties including properties involving timers is considered. Higher level safety properties such as no-collision and no-derailment are also considered for enumeration.