The completeness and correctness of requirement modeling is the crucial factor that affecting the success of the system development. Use case diagram is the standard tool for modeling the use requirement for the objected-oriented systems analysis and design. However, to model the sequence diagram in the platform independent model (PIM) stage is still not a straightforward task to identify objects, operations and their relationships from the use case diagram. Robustness analysis has been proposed to bridge this gap between the user requirement modeling and the PIM modeling. However, the detailed guideline for the robustness analysis is lacking, while it is important for designer to enhance the completeness and correctness of the user requirement modeling. To alleviate the forgoing problem, we proposed that use case diagram, activity diagram and robustness diagram are used to represent the use requirement. Once a use case diagram is constructed, the activity diagram is used to describe the activity flow and the associated input/output of each use case. Finally, the robustness analysis with the guideline proposed is used to help the identification of boundary, control, and entity objects and enhance the completeness of the user requirement. The outcome can then be used to construct a sequence diagram in the PIM. A real-world case is presented to illustrate the feasibility of using the proposed method. With this methodology, the system developer can enhance the completeness and correctness of user requirement efficiently and thereby reduce the risk of success development failure.

The MAPK cascade is responsible for transmitting information in the cytoplasm of the cell and regulating important fate decisions like cell division and apoptosis. Due to scarce experimental data and limited knowledge about many complex biochemical processes, existing MAPK pathway models, which exhibit bistability, have a significant structural uncertainty. Often, small perturbations of network interactions or components can reduce the bistable region significantly or make it even disappear and small fluctuations of the input can make the system switch back, which reflects its low robustness. However, real biological systems have developed significant robustness through evolution and this robustness should be reflected by the models. The main goal of the present thesis is the development of a methodology for increasing the robustness of biochemical models, which exhibit bistability. Based on modifying existing network interactions or introducing new interactions to the system, several methods for both internal and external robustification are proposed. Internal robustness is addressed through a sensitivity analysis, which deals with a linearization of the model and can be used sequentially to introduce multiple modifications to the model. The methods for external robustness improvement are based on eigenvalue placement and slope modification (drawing on the linear model) and on the identification of feedback structures (nonlinear model). Further, a way to integrate static interaction changes to the nonlinear model, so that these perturbations have only a local impact on its behavior, is proposed. The application of the methods to existing MAPK models shows that, by introducing small modifications, the internal and external robustness of models can be increased significantly and thus provides knowledge about complex dynamics and interactions that play a key role for the inherent robustness of real biological systems. Furthermore, by employing a robustness analysis, stable steady-state branches can be recovered and bistability can be induced.

This thesis deals with safety verification analysis of collision avoidance systems for unmanned vehicles. The safety of the vehicle is dependent on collision avoidance algorithms and associated control laws, and it must be proven that the collision avoidance algorithms and controllers are functioning correctly in all nominal conditions, various failure conditions and in the presence of possible variations in the vehicle and operational environment. The current widely used exhaustive search based approaches are not suitable for safety analysis of autonomous vehicles due to the large number of possible variations and the complexity of algorithms and the systems. To address this topic, a new optimisation-based verification method is developed to verify the safety of collision avoidance systems. The proposed verification method formulates the worst case analysis problem arising the verification of collision avoidance systems into an optimisation problem and employs optimisation algorithms to automatically search the worst cases. Minimum distance to the obstacle during the collision avoidance manoeuvre is defined as the objective function of the optimisation problem, and realistic simulation consisting of the detailed vehicle dynamics, the operational environment, the collision avoidance algorithm and low level control laws is embedded in the optimisation process. This enables the verification process to take into account the parameters variations in the vehicle, the change of the environment, the uncertainties in sensors, and in particular the mismatching between model used for developing the collision avoidance algorithms and the real vehicle. It is shown that the resultant simulation based optimisation problem is non-convex and there might be many local optima. To illustrate and investigate the proposed optimisation based verification process, the potential field method and decision making collision avoidance method are chosen as an obstacle avoidance candidate technique for verification study. Five benchmark case studies are investigated in this thesis: static obstacle avoidance system of a simple unicycle robot, moving obstacle avoidance system for a Pioneer 3DX robot, and a 6 Degrees of Freedom fixed wing Unmanned Aerial Vehicle with static and moving collision avoidance algorithms. It is proven that although a local optimisation method for nonlinear optimisation is quite efficient, it is not able to find the most dangerous situation. Results in this thesis show that, among all the global optimisation methods that have been investigated, the DIviding RECTangle method provides most promising performance for verification of collision avoidance functions in terms of guaranteed capability in searching worst scenarios.

This thesis deals with the application of optimisation based Validation and Verification (V&V) analysis on aerospace vehicles in order to determine their worst case performance metrics. To this end, three aerospace models relating to satellite and launcher vehicles provided by European Space Agency (ESA) on various projects are utilised. As a means to quicken the process of optimisation based V&V analysis, surrogate models are developed using polynomial chaos method. Surro- gate models provide a quick way to ascertain the worst case directions as computation time required for evaluating them is very small. A sin- gle evaluation of a surrogate model takes less than a second. Another contribution of this thesis is the evaluation of operational safety margin metric with the help of surrogate models. Operational safety margin is a metric defined in the uncertain parameter space and is related to the distance between the nominal parameter value and the first instance of performance criteria violation. This metric can help to gauge the robustness of the controller but requires the evaluation of the model in the constraint function and hence could be computationally intensive. As surrogate models are computationally very cheap, they are utilised to rapidly compute the operational safety margin metric. But this metric focuses only on finding a safe region around the nominal parameter value and the possibility of other disjoint safe regions are not explored. In order to find other safe or failure regions in the param- eter space, the method of Bernstein expansion method is utilised on surrogate polynomial models to help characterise the uncertain param- eter space into safe and failure regions. Furthermore, Binomial failure analysis is used to assign failure probabilities to failure regions which might help the designer to determine if a re-design of the controller is required or not. The methodologies of optimisation based V&V, surrogate modelling, operational safety margin, Bernstein expansion method and risk assessment have been combined together to form the WCAT-II MATLAB toolbox.

Submitted by Maria Aparecida (cidazen@gmail.com) on 2017-04-12T12:36:08Z No. of bitstreams: 1 Romario ferreira de Matos.pdf: 289293 bytes, checksum: 6e794c84f3b40406735e5e1ba5ad15b4 (MD5) / Made available in DSpace on 2017-04-12T12:36:08Z (GMT). No. of bitstreams: 1 Romario ferreira de Matos.pdf: 289293 bytes, checksum: 6e794c84f3b40406735e5e1ba5ad15b4 (MD5) Previous issue date: 2017-02-21 / The objective of this study was to evaluate the accuracy and precision of the apparent dry matter digestibility estimates obtained using internal and external markers in sheep fed diets containing sugar-cane-tip hay or treated with urea or calcium. Also, it was evaluated the robustness of the markers in relation to the variation of dry matter intake (CMS) and the mean live weight (PV) of the animals. Were used 20 male, uncastrated, mestizos without defined breed pattern (SPRD) x Santa Inês, with a mean live weight of 29.64 ± 5.53 kg and age of approximately 12 months, in randomized block design, based on live weight. Estimates of total fecal dry matter yield and digestibility of DM and nutrients were performed using the method of total fecal collection and using internal markers, represented by the indigestible constituents MSi, FDNi and FDAi and the external indicator titanium dioxide (TiO2). Accuracy of the markers was evaluated by the mean bias, which is the difference between the value predicted by the indicator and the value observed by the total collection of feces, the most accurate indicator being considered, which presents a mean bias closer to zero. Precision, a measure of dispersion between predicted and observed values, represents the mean distance variability between these values and was evaluated by the mean square root of the prediction error. The robustness analysis of each indicator was performed by regressing the bias according to the CMS variables and PV. TiO2 presented a faecal recovery rate (TRF) of less than 100% and for the internal markers MSi, FDNi and FDAi. TRF was greater than 100%. There was a difference for the mean bias (P <0.05), which shows that there are differences in the markers regarding their accuracy for fecal yield estimates and, consequently, estimates of apparent dry matter digestibility (DMS) in sheep. The estimated of digestibility of dry matter (DMS) for internal markers MSi, FDNi and FDAi are recommended because the results obtained by these are not influenced by the CMS and PV. / Este estudio tuvo como objetivo evaluar la exactitud y precisión de las estimaciones de la digestibilidad materia seca aparente obtenida con el uso de indicadores internos y externos en ovejas alimentado con punta heno caña de azúcar sin tratar o tratado con urea u óxido de calcio. Además, se evaluó la robustez de los indicadores en relación con la variación del consumo de materia seca (CMS) y el peso vivo (PV) promedio animales. 20 ovejas machos se utilizaron patrón sin castrar sin mestizo raza definida (SPRD) x St. Agnes, con un peso promedio 29,64 ± 5,53 kg y envejecido aproximadamente 12 meses en el diseño de bloques al azar, con base en el peso viva. Las estimaciones de la producción total de materia seca fecal y la digestibilidad de la materia seca y los nutrientes se llevaron a cabo por el método de recogida de heces total y uso de indicadores internos, representados por los componentes indigeribles MSi, INDF y FDAi y dióxido de titanio indicador externo (TiO2), y los indicadores y tratamientos bloques de animales. La exactitud de los indicadores se evaluó por el sesgo de la media, que es el diferencia entre el valor predicho por el indicador y el valor observado por la colección total heces, se considera el indicador más precisa que la presente sesgo media más cerca de cero. La precisión, una medida de valores de dispersión entre el predicho y variabilidad observada es la distancia media entre estos valores y era evaluadas por la raíz cuadrada media del error de predicción. El análisis de robustez de cada indicador se realizó una regresión a las variables de polarización de función CMS y el peso corporal promedio. TiO2 mostró tasa de recuperación fecal (FRR) de menos de 100% y para el indicadores internos MSi, INDF y FDAi la TRF fue mayor que 100%. Hubo diferencias para el sesgo de la media (P <0,05), que no muestra ninguna diferencia como el indicador de su precisión para la estimación de la producción fecal y por lo tanto las estimaciones la digestibilidad de la materia seca (DMD) en bovinos. Los indicadores internos MSI INDF y FDAi se recomiendan para la estimación de la producción total de crudo y se seca fecal DM, ya que los resultados de estos no son CMS influenciada por el peso vivo del animal. / Objetivou-se avaliar a acurácia e precisão das estimativas da digestibilidade aparente da matéria seca obtidas com uso de indicadores internos e externos em ovinos alimentados com dietas contendo feno de ponta de cana-de-açúcar não tratado ou tratado com ureia ou óxido de cálcio. Também, foi avaliada a robustez dos indicadores em relação à variação do consumo de matéria seca (CMS) e ao peso vivo (PV) médio dos animais. Foram utilizados 20 ovinos machos, não castrados, mestiços sem padrão de raça definido (SPRD) x Santa Inês, com peso vivo médio 29,64±5,53 kg e idade de aproximadamente 12 meses, em delineamento em blocos ao acaso, com base no peso vivo. As estimativas da produção total de matéria seca fecal e da digestibilidade da MS e dos nutrientes foram realizadas pelo método da coleta total de fezes e com uso de indicadores internos, representados pelos constituintes indigestíveis MSi, FDNi e FDAi e do indicador externo dióxido de titânio (TiO2), sendo os indicadores os tratamentos e os animais os blocos. A acurácia dos indicadores foi avaliada pelo viés médio, que é a diferença entre o valor predito pelo indicador e o valor observado pela coleta total de fezes, sendo considerado o indicador mais acurado o que apresentar viés médio mais próximo de zero. A precisão, uma medida de dispersão entre os valores preditos e observados, representa a variabilidade média da distância entre esses valores e foi avaliada pela raiz quadrada média do erro de predição. A análise de robustez de cada indicador foi realizada regredindo-se o viés em função das variáveis CMS e peso vivo médio. O TiO2 apresentou taxa de recuperação fecal (TRF) inferior a 100% e para os indicadores internos MSi, FDNi e FDAi a TRF foi superior a 100%. Houve diferença para o viés médios (P<0,05), o que demonstra haver diferença dos indicadores quanto a sua acurácia para as estimativas da produção fecal e, consequentemente, das estimativas da digestibilidade aparente da matéria seca (DMS) em ovinos. Os indicadores internos MSi, FDNi e FDAi são recomendados para estimativas da produção total de matéria seca fecal e da digestibilidade da MS, pois os resultados obtidos por estes não são influenciados pelo CMS e peso vivo do animal.

Software systems are ubiquitous in today's world and yet, remain vulnerable to the fallibility of human programmers as well as the unpredictability of their operating environments. The overarching goal of this dissertation is to develop algorithms to enable automated and efficient design and analysis of reliable programs. In the first and second parts of this dissertation, we focus on the development of programs that are free from programming errors. The intent is not to eliminate the human programmer, but instead to complement his or her expertise, with sound and efficient computational techniques, when possible. To this end, we make contributions in two specific domains. Program debugging --- the process of fault localization and error elimination from a program found to be incorrect --- typically relies on expert human intuition and experience, and is often a lengthy, expensive part of the program development cycle. In the first part of the dissertation, we target automated debugging of sequential programs. A broad and informal statement of the (automated) program debugging problem is to suitably modify an erroneous program, say P, to obtain a correct program, say P'. This problem is undecidable in general; it is hard to formalize; moreover, it is particularly challenging to assimilate and mechanize the customized, expert programmer intuition involved in the choices made in manual program debugging. Our first contribution in this domain is a methodical formalization of the program debugging problem, that enables automation, while incorporating expert programmer intuition and intent. Our second contribution is a solution framework that can debug infinite-state, imperative, sequential programs written in higher-level programming languages such as C. Boolean programs, which are smaller, finite-state abstractions of infinite-state or large, finite-state programs, have been found to be tractable for program verification. In this dissertation, we utilize Boolean programs for program debugging. Our solution framework involves two main steps: (a) automated debugging of a Boolean program, corresponding to an erroneous program P, and (b) translation of the corrected Boolean program into a correct program P'. Shared-memory concurrent programs are notoriously difficult to write, verify and debug; this makes them excellent targets for automated program completion, in particular, for synthesis of synchronization code. Extant work in this domain has focused on either propositional temporal logic specifications with simplistic models of concurrent programs, or more refined program models with the specifications limited to just safety properties. Moreover, there has been limited effort in developing adaptable and fully-automatic synthesis frameworks that are capable of generating synchronization at different levels of abstraction and granularity. In the second part of this dissertation, we present a framework for synthesis of synchronization for shared-memory concurrent programs with respect to temporal logic specifications. In particular, given a concurrent program composed of synchronization-free processes, and a temporal logic specification describing their expected concurrent behaviour, we generate synchronized processes such that the resulting concurrent program satisfies the specification. We provide the ability to synthesize readily-implementable synchronization code based on lower-level primitives such as locks and condition variables. We enable synchronization synthesis of finite-state concurrent programs composed of processes that may have local and shared variables, may be straight-line or branching programs, may be ongoing or terminating, and may have program-initialized or user-initialized variables. We also facilitate expression of safety and liveness properties over both control and data variables by proposing an extension of propositional computation tree logic. Most program analyses, verification, debugging and synthesis methodologies target traditional correctness properties such as safety and liveness. These techniques typically do not provide a quantitative measure of the sensitivity of a computational system's behaviour to unpredictability in the operating environment. We propose that the core property of interest in reasoning in the presence of such uncertainty is robustness --- small perturbations to the operating environment do not change the system's observable behavior substantially. In well-established areas such as control theory, robustness has always been a fundamental concern; however, the techniques and results therein are not directly applicable to computational systems with large amounts of discretized, discontinuous behavior. Hence, robustness analysis of software programs used in heterogeneous settings necessitates development of new theoretical frameworks and algorithms. In the third part of this dissertation, we target robustness analysis of two important classes of discrete systems --- string transducers and networked systems of Mealy machines. For each system, we formally define robustness of the system with respect to a specific source of uncertainty. In particular, we analyze the behaviour of transducers in the presence of input perturbations, and the behaviour of networked systems in the presence of channel perturbations. Our overall approach is automata-theoretic, and necessitates the use of specialized distance-tracking automata for tracking various distance metrics between two strings. We present constructions for such automata and use them to develop decision procedures based on reducing the problem of robustness verification of our systems to the problem of checking the emptiness of certain automata. Thus, the system under consideration is robust if and only if the languages of particular automata are empty. / text

Due to their frictionless operation active magnetic bearings (AMBs) are essential components in high-speed rotating machinery. Active magnetic control of a high speed rotating rotor requires precise knowledge of its position. Self-sensing endeavours to eliminate the required position sensors by deducing the rotor’s position from the voltages and currents with which it is levitated. For self-sensing AMBs to be of practical worth, they have to be robust. Robustness analysis aims to quantify a control system’s tolerance for uncertainty. In this study the stability margin of a two degree-of-freedom self-sensing AMB is estimated by means of μ-analysis. Detailed black-box models are developed for the main subsystems in the AMB by means of discrete-time system identification. Suitable excitation signals are generated for system identification in cognisance of frequency induced nonlinear behaviour of the AMB. Novel graphs that characterize an AMB’s behaviour for input signals of different amplitudes and frequency content are quite useful in this regard. In order to obtain models for dynamic uncertainty in the various subsystems (namely the power amplifier, self-sensing module and AMB plant), the identified models are combined to form a closed-loop model for the self-sensing AMB. The response of this closed-loop model is compared to the original AMB’s response and models for the dynamic uncertainty are empirically deduced. Finally, the system’s stability margin for the modelled uncertainty is estimated by means of μ-analysis. The potentially destabilizing effects of parametric uncertainty in the controller coefficients as well as dynamic uncertainty in the AMB plant and self-sensing module are examined. The resultant μ-analyses show that selfsensing AMBs are much less robust for parametric uncertainty in the controller than AMBs equipped with sensors. The μ-analyses for dynamic uncertainty confirm that self-sensing AMBs are rather sensitive for variations in the plant or the self-sensing algorithm. Validation of the stability margins estimated by μ-analysis reveal that μ-analysis is overoptimistic for parametric uncertainty on the controller and conservative for dynamic uncertainty. (Validation is performed by means of Monte Carlo simulations.) The accuracy of μ-analysis is critically dependent on the accuracy of the uncertainty model and the degree to which the system is linear or not. If either of these conditions are violated, μ-analysis is essentially worthless. / Thesis (Ph.D. (Electronical Engineering))--North-West University, Potchefstroom Campus, 2010

Due to their frictionless operation active magnetic bearings (AMBs) are essential components in high-speed rotating machinery. Active magnetic control of a high speed rotating rotor requires precise knowledge of its position. Self-sensing endeavours to eliminate the required position sensors by deducing the rotor’s position from the voltages and currents with which it is levitated. For self-sensing AMBs to be of practical worth, they have to be robust. Robustness analysis aims to quantify a control system’s tolerance for uncertainty. In this study the stability margin of a two degree-of-freedom self-sensing AMB is estimated by means of μ-analysis. Detailed black-box models are developed for the main subsystems in the AMB by means of discrete-time system identification. Suitable excitation signals are generated for system identification in cognisance of frequency induced nonlinear behaviour of the AMB. Novel graphs that characterize an AMB’s behaviour for input signals of different amplitudes and frequency content are quite useful in this regard. In order to obtain models for dynamic uncertainty in the various subsystems (namely the power amplifier, self-sensing module and AMB plant), the identified models are combined to form a closed-loop model for the self-sensing AMB. The response of this closed-loop model is compared to the original AMB’s response and models for the dynamic uncertainty are empirically deduced. Finally, the system’s stability margin for the modelled uncertainty is estimated by means of μ-analysis. The potentially destabilizing effects of parametric uncertainty in the controller coefficients as well as dynamic uncertainty in the AMB plant and self-sensing module are examined. The resultant μ-analyses show that selfsensing AMBs are much less robust for parametric uncertainty in the controller than AMBs equipped with sensors. The μ-analyses for dynamic uncertainty confirm that self-sensing AMBs are rather sensitive for variations in the plant or the self-sensing algorithm. Validation of the stability margins estimated by μ-analysis reveal that μ-analysis is overoptimistic for parametric uncertainty on the controller and conservative for dynamic uncertainty. (Validation is performed by means of Monte Carlo simulations.) The accuracy of μ-analysis is critically dependent on the accuracy of the uncertainty model and the degree to which the system is linear or not. If either of these conditions are violated, μ-analysis is essentially worthless. / Thesis (Ph.D. (Electronical Engineering))--North-West University, Potchefstroom Campus, 2010

The purpose of this thesis was to design controllers by using H1 and &sup1 / control strategies in order to suppress the free and forced vibrations of smart structures. The smart structures analyzed in this study were the smart beam and the smart &macr / n. They were aluminum passive structures with surface bonded PZT (Lead-Zirconate-Titanate) patches. The structures were considered in clamped-free con&macr / guration. The &macr / rst part of this study focused on the identi&macr / cation of nominal system models of the smart structures from the experimental data. For the experimentally identi&macr / ed models the robust controllers were designed by using H1 and &sup1 / -synthesis strategies. In the second part, the controller implementation was carried out for the suppression of free and forced vibrations of the smart structures. Within the framework of this study, a Smart Structures Laboratory was established in the Aerospace Engineering Department of METU. The controller implementations were carried out by considering two di&reg / erent experimental set-ups. In the &macr / rst set-up the controller designs were based on the strain measurements. In the second approach, the displacement measurements, which were acquired through laser displacement sensor, were considered in the controller design. The &macr / rst two &deg / exural modes of the smart beam were successfully controlled by using H1 method. The vibrations of the &macr / rst two &deg / exural and &macr / rst torsional modes of the smart &macr / n were suppressed through the &sup1 / -synthesis. Satisfactory attenuation levels were achieved for both strain measurement and displacement measurement applications.

An efficient robustness analysis for the VEGA launch vehicle is essential to minimize the potential system failure during the ascending phase. Monte Carlo sampling method is usually considered as a reliable strategy in industry if the sampling size is large enough. However, due to a large number of uncertainties and a long response time for a single simulation, exploring the entire uncertainties sufficiently through Monte Carlo sampling method is impractical for VEGA launch vehicle. In order to make the robustness analysis more efficient when the number of simulation is limited, the quasi-Monte Carlo(Sobol, Faure, Halton sequence) and heuristic algorithm(Differential Evolution) are proposed. Nevertheless, the reasonable number of samples for simulation is still much smaller than the minimal number of samples for sufficient exploration. To further improve the efficiency of robustness analysis, the redundant uncertainties are sorted out by sensitivity analysis. Only the dominant uncertainties are remained in the robustness analysis. As all samples for simulation are discrete, many uncertainty spaces are not explored with respect to its objective function by sampling or optimization methods. To study these latent information, the meta-model trained by Gaussian Process is introduced. Based on the meta-model, the expected maximum objective value and expected sensitivity of each uncertainties can be analyzed for robustness analysis with much higher efficiency but without loss much accuracy.