No description available.

This thesis proposes a systematic, hierarchical, optimization based semi-formal equivalence checking methodology for large analog/mixed signal systems such as phase locked loops (PLL), analog to digital convertors (ADC) and input/output (I/O) circuits. I propose to verify the equivalence between a behavioral model and its electrical implementation over a limited, but highly likely, input space defined as the Constrained Behavioral Input Space. Furthermore, I clearly distinguish between the behavioral and electrical domains and define mapping functions between the two domains to allow for calculation of deviation between the behavioral and electrical implementation. The verification problem is then formulated as an optimization problem which is solved by interfacing a sequential quadratic programming (SQP) based optimizer with commercial circuit simulation tools, such as CADENCE SPECTRE. The proposed methodology is then applied for equivalence checking of a PLL as a test case and results are shown which prove the correctness of the proposed methodology.

System verification is a critical process in the development of engineered systems. Engineers gain confidence in the correct functionality of the system by executing system verification. Traditionally, system verification is implemented by conducting a verification strategy (VS) consisting of verification activities (VA). A VS can be generated using industry standards, expert experience, or quantitative-based methods. However, two limitations exist in these previous studies. First, as an essential part of system verification, correction activities (CA) are used to correct system errors or defects identified by VAs. However, CAs are usually simplified and treated as a component associated with VAs instead of independent decisions. Even though this simplification may accelerate the VS design, it results in inferior VSs because the optimization of correction decisions is ignored. Second, current methods have not handled the issue of complex engineered systems. As the number of activities increases, the magnitude of the possible VSs becomes so large that finding the optimal VS is impossible or impractical. Therefore, these limitations leave room for improving the VS design, especially for complex engineered systems. This dissertation presents a joint verification-correction model (JVCM) to address these gaps. The basic idea of this model is to provide an engineering paradigm for complex engineered systems that simultaneously consider decisions about VAs and CAs. The accompanying research problem is to develop a modeling and analysis framework to solve for joint verification-correction strategies (JVCS). This dissertation aims to address them in three steps. First, verification processes (VP) are modeled mathematically to capture the impacts of VAs and CAs. Second, a JVCM with small strategy spaces is established with all conditions of a VP. A modified backward induction method is proposed to solve for an optimal JVCS in small strategy spaces. Third, a UCB-based tree search approach is designed to find near-optimal JVCSs in large strategy spaces. A case study is conducted and analyzed in each step to show the feasibility of the proposed models and methods. / Doctor of Philosophy / System verification is a critical step in the life cycle of system development. It is used to check that a system conforms to its design requirements. Traditionally, system verification is implemented by conducting a verification strategy (VS) consisting of verification activities (VA). A VS can be generated using industry standards, expert experience, or quantitative-based methods. However, two limitations exist in these methods. First, as an essential part of system verification, correction activities (CA) are used to correct system errors or defects identified by VAs. However, CAs are usually simplified and treated as remedial measures that depend on the results of VAs instead of independent decision choices. Even though this simplification may accelerate the VS design, it results in inferior VSs because the optimization of correction decisions is ignored. Second, current methods have not handled the issue of large systems. As the number of activities increases, the total number of possible VSs becomes so large that it is impossible to find the optimal solution. Therefore, these limitations leave room for improving the VS design, especially for large systems. This dissertation presents a joint verification-correction model (JVCM) to address these gaps. The basic idea of this model is to provide a paradigm for large systems that simultaneously consider decisions about VAs and CAs. The accompanying research problem is to develop a modeling and analysis framework to solve for joint verification-correction strategies (JVCS). This dissertation aims to address them in three steps. First, verification processes (VP) are modeled mathematically to capture the impacts of VAs and CAs. Second, a JVCM with small strategy spaces is established with all conditions of a VP. A modified backward induction method is proposed to solve for an optimal JVCS in small strategy spaces. Third, a UCB-based tree search approach is designed to find near-optimal JVCSs in large strategy spaces. A case study is conducted and analyzed in each step to show the feasibility of the proposed models and methods.

Over the past decade the capabilities of autonomous systems have been steadily increasing. Unmanned systems are moving from systems that are predominantly remotely operated, to systems that include a basic decision making capability. This is a trend that is expected to continue with autonomous systems making decisions in increasingly complex environments, based on more abstract, higher-level missions and goals. These changes have significant implications for how these systems should be designed and engineered. Indeed, as the goals and tasks these systems are to achieve become more abstract, and the environments they operate in become more complex, are current approaches to verification and validation sufficient? Domain Specific Modelling is a key technology for the verification of autonomous systems. Verifying these systems will ultimately involve understanding a significant number of domains. This includes goals/tasks, environments, systems functions and their associated performance. Relational Model Transformations provide a means to utilise, combine and check models for consistency across these domains. In this thesis an approach that utilises relational model transformation technologies for systems verification, Systems MDD, is presented along with the results of a series of trials conducted with an existing relational model transformation language (QVT-Relations). These trials identified a number of problems with existing model transformation languages, including poorly or loosely defined semantics, differing interpretations of specifications across different tools and the lack of a guarantee that a model transformation would generate a model that was compliant with its associated meta-model. To address these problems, two related solvers were developed to assist with realising the Systems MDD approach. The first solver, MMCS, is concerned with partial model completion, where a partial model is defined as a model that does not fully conform with its associated meta-model. It identifies appropriate modifications to be made to a partial model in order to bring it into full compliance. The second solver, TMPT, is a relational model transformation engine that prioritises target models. It considers multiple interpretations of a relational transformation specification, chooses an interpretation that results in a compliant target model (if one exists) and, optionally, maximises some other attribute associated with the model. A series of experiments were conducted that applied this to common transformation problems in the published literature.

Hybrid testing is an emerging technique for system emulation that uses a transfer system composed of actuators and sensors to couple physical tests of a critical component or substructure to a numerical simulation of the remainder of a system and its complete operating environment. The realisation of modern real-time hybrid tests for multi-body contact-impact problems often proves infeasible due to (i) hardware with bandwidth limitations and (ii) the unavailability of control schemes that provide satisfactory force and position tracking in the presence of sharp non-linearities or discontinuities. Where this is the case, the possibility of employing a pseudo-dynamic technique remains, enabling tests to be conducted on an enlarged time scale thus relaxing bothbandwidth and response time constraints and providing inherent loop stability. Exploiting the pseudo-dynamic technique, this thesis presents the development of Robotic Pseudo-Dynamic Testing (RPsDT), a dedicated method that specifically targets the realisation of hybrid tests for multi-body contact-impact problems using commercial off- the shelve (COTS) industrial robotic manipulators. The RPsDT method is evaluated in on-ground studies of air-to-air refuelling (AAR) maneuvers with probe-hose-drogue systems where the critical contact and coupling phase is tested pseudo-dynamicallywith full-scale refuelling hardware while the flight regime is emulated in simulation. It is shown that the RPsDT method can faithfully reproduce the dominant contact impact phenomena between probe and drogue while minor discrepancies result from the absence of rate-dependant damping in the force feedback measurements. In combination with full-speed robot controlled contact tests, reliable estimates for impact forces, strain distributions and drogue responses to off-centre hits are obtained providing extensive improvements over current predictive capabilities for the in-flight behaviour of refuelling hardware and it is concluded that the technique shows great promise for industrial applications.

Nous présentons une nouvelle approche pour formuler et calculer le temps de séparation des événements utilisé dans l’analyse et la vérification de différents systèmes cycliques et acycliques sous des contraintes linéaires-min-max avec des composants ayant des délais finis et infinis. Notre approche consiste à formuler le problème sous la forme d’un programme entier mixte, puis à utiliser le solveur Cplex pour avoir les temps de séparation entre les événements. Afin de démontrer l’utilité en pratique de notre approche, nous l’avons utilisée pour la vérification et l’analyse d’une puce asynchrone d’Intel de calcul d’équations différentielles. Comparée aux travaux précédents, notre approche est basée sur une formulation exacte et elle permet non seulement de calculer le maximum de séparation, mais aussi de trouver un ordonnancement cyclique et de calculer les temps de séparation correspondant aux différentes périodes possibles de cet ordonnancement. / We present a new approach for formulating and computing time separation of events used for timing analysis of different types of cyclic and acyclic systems that obey to linear-min-max type constraints with finite and infinite bounded component delays. Our approach consists of formulating the problem as a mixed integer program then using the solver Cplex to get time separations between events. In order to demonstrate the practical use of our approach we apply it for the verification and analysis of an Intel asynchronous differential equation solver chip. Compared to previous work, our approach is based on exact formulation and it allows not only the maximum separation computing, but it can also provide cyclic schedules and compute bound on possible periods of such schedules.

Nous présentons une nouvelle approche pour formuler et calculer le temps de séparation des événements utilisé dans l’analyse et la vérification de différents systèmes cycliques et acycliques sous des contraintes linéaires-min-max avec des composants ayant des délais finis et infinis. Notre approche consiste à formuler le problème sous la forme d’un programme entier mixte, puis à utiliser le solveur Cplex pour avoir les temps de séparation entre les événements. Afin de démontrer l’utilité en pratique de notre approche, nous l’avons utilisée pour la vérification et l’analyse d’une puce asynchrone d’Intel de calcul d’équations différentielles. Comparée aux travaux précédents, notre approche est basée sur une formulation exacte et elle permet non seulement de calculer le maximum de séparation, mais aussi de trouver un ordonnancement cyclique et de calculer les temps de séparation correspondant aux différentes périodes possibles de cet ordonnancement. / We present a new approach for formulating and computing time separation of events used for timing analysis of different types of cyclic and acyclic systems that obey to linear-min-max type constraints with finite and infinite bounded component delays. Our approach consists of formulating the problem as a mixed integer program then using the solver Cplex to get time separations between events. In order to demonstrate the practical use of our approach we apply it for the verification and analysis of an Intel asynchronous differential equation solver chip. Compared to previous work, our approach is based on exact formulation and it allows not only the maximum separation computing, but it can also provide cyclic schedules and compute bound on possible periods of such schedules.

The research in this thesis is undertaken by observing that modern systems are becoming more and more complex and safety-critical due to the increasing requirements on system smartness and autonomy, and as a result health monitoring system needs to be developed to meet the requirements on system safety and reliability. The state-of-the-art approaches to monitoring system status are model based Fault Diagnosis (FD) systems, which can fuse the advantages of system physical modelling and sensors' characteristics. A number of model based FD approaches have been proposed. The conventional residual based approaches by monitoring system output estimation errors, however, may have certain limitations such as complex diagnosis logic for fault isolation, less sensitiveness to system faults and high computation load. More importantly, little attention has been paid to the problem of fault diagnosis system verification which answers the question that under what condition (i.e., level of uncertainties) a fault diagnosis system is valid. To this end, this thesis investigates the design and verification of fault diagnosis algorithms. It first highlights the differences between two popular FD approaches (i.e., residual based and fault estimation based) through a case study. On this basis, a set of uncertainty estimation algorithms are proposed to generate fault estimates according to different specifications after interpreting the FD problem as an uncertainty estimation problem. Then FD algorithm verification and threshold selection are investigated considering that there are always some mismatches between the real plant and the mathematical model used for FD observer design. Reachability analysis is drawn to evaluate the effect of uncertainties and faults such that it can be quantitatively verified under what condition a FD algorithm is valid. First the proposed fault estimation algorithms in this thesis, on the one hand, extend the existing approaches by pooling the available prior information such that performance can be enhanced, and on the other hand relax the existence condition and reduce the computation load by exploiting the reduced order observer structure. Second, the proposed framework for fault diagnosis system verification bridges the gap between academia and industry since on the one hand a given FD algorithm can be verified under what condition it is effective, and on the other hand different FD algorithms can be compared and selected for different application scenarios. It should be highlighted that although the algorithm design and verification are for fault diagnosis systems, they can also be applied for other systems such as disturbance rejection control system among many others.

The conventional approach to validate the analog and mixed signal designs utilizes extensive SPICE-level simulations. The main challenge in this approach is to know when all important corner cases have been simulated. An alternate approach is to use the formal verification techniques. Formal verification techniques have gained wide spread popularity in the digital design domain; but in case of analog and mixed signal designs, a large number of test scenarios need to be designed to generate sufficient simulation traces to test out all the specified system behaviours. Analog and mixed signal designs can be formally modeled as hybrid systems and therefore techniques used for formal analysis and verification of hybrid systems can be applied to the analog and mixed signal designs. Generally, formal verification tools for hybrid systems work at the abstract level where we model the systems in terms of differential equations or algebraic equations. However the analog and mixed signal system designers are very comfortable in designing the circuits at the transistor level. To bridge the gap between abstraction level verification and the designs validation which has been implemented at the transistor level, the very important issue we need to address is: Can we formally verify the circuits at the transistor level itself? For this we have proposed a framework for doing the formal verification of analog and mixed signal designs using SPICE simulation traces in one of the hybrid systems formal verification tools (i.e. Checkmate from CMU). An extension to a formal verification approach of hybrid systems is proposed to verify analog and mixed signal (AMS) designs. AMS designs can be formally modeled as hybrid systems and therefore lend themselves to the formal analysis and verification techniques applied to hybrid systems. The proposed approach employs simulation traces obtained from an actual design implementation of AMS circuit blocks (for example, in the form of SPICE netlists) to carry out formal analysis and verification. This enables the same platform used for formally validating an abstract model of an AMS design to be also used for validating its different refinements and design implementation, thereby providing a simple route to formal verification at different levels of implementation. Our approach has been illustrated through the case studies using simulation traces form the different frameworks i.e. Simulink/Stateflow framework and the SPICE simulation traces. We demonstrate the feasibility of our approach around the Checkmate and the case studies for hybrid systems and the analog and mixed signal designs.