Integrated circuits have traveled a long way from being a general purpose microprocessor to an application specific circuit. It has become an integral part of the modern era of technology that we live in. As the applications and their complexities are increasing rapidly every day, so are the sizes of these circuits. With the increase in the design size, the associated testing effort to verify these designs is also increased. The goal of this thesis is to leverage some of the static analysis techniques to reduce the effort of testing and verification at the register transfer level. Studying a design at register transfer level gives exposure to the relational information for the design which is inaccessible at the structural level. In this thesis, we present a way to generate a Data Dependency Graph and a Control Flow Graph out of a register transfer level description of a circuit description. Next, the generated graphs are used to perform relation mining to improve the test generation process in terms of speed, branch coverage and number of test vectors generated. The generated control flow graph gives valuable information about the flow of information through the circuit design. We are using this information to create a framework to improve the branch reachability analysis mainly in terms of the speed. We show the efficiency of our methods by running them through a suite of ITC'99 benchmark circuits. / Master of Science / In this era of modern technology, digital circuits and microprocessors have become an unavoidable part of everyone’s life. The role of these circuits is becoming more and more critical as they are running a lot of critical services for us. Testing and verifying the design has been a very important aspect in the designing of these circuits. With the increasing number of its applications and the advancement of the technology, the size and complexity of the designs have also increased. It has imposed a need to test the design at a stage when it is easy to test and easy to fix also. There have been a lot of research focused on automatically generating the test pattern at an early stage of development and the work presented in this thesis is an effort to take it one step further in the process. The method proposed in this work is taking advantage of the fact that a design speaks for itself and can give a lot of information if looked at carefully. We present a way to extract important information about the data dependency and its flow through the design. With the help of this information, we are generating relations between the design elements which can aid the test generation process to achieve its goal more efficiently. We are also using this information to help in proving that some part of the design is inaccessible. We show the efficiency of our method by running them through benchmark designs.

L’analyse d’accessibilité est une des composantes de l’analyse de modèles. Elle consiste à modéliser un système complexe par trois ensembles : le langage initial, le langage des configurations indésirables et un système de réécriture. Le langage initial et le langage des configurations indésirables sont des ensembles de termes. Un terme est un mot mais construit à partir de symboles d’arités supérieures à 1. Le système de réécriture représente la dynamique du système complexe. C’est un ensemble de règles qui permettent d’obtenir un nouveau terme à partir d’un terme original. Pour effectuer une analyse d’accessibilité à partir de cette modélisation, on peut calculer l’ensemble des configurations accessibles. Cet ensemble aussi appelé ensemble des descendants est obtenu en appliquant le système de réécriture sur le langage initial jusqu’à ne plus obtenir de nouveaux termes. Une fois l’ensemble des descendants calculé, il reste à faire l’intersection entre celui-ci et l’ensemble des configurations indésirables. Si cette intersection est vide, alors il n’y a pas de configuration indésirable accessible, sinon les configurations présentes dans cette intersection sont accessibles. Cependant, l’ensemble des descendants n’est pas calculable dans le cas général. Pour contourner ce problème, nous calculons une sur-approximation des descendants. Ainsi, si l’intersection est vide, cela signifie toujours qu’aucune configuration indésirable n’est accessible. A contrario, s’il existe un terme dans l’intersection, il n’est pas possible de déterminer s’il s’agit d’un faux positif ou d’une configuration indésirable accessible. La précision de la sur-approximation est alors déterminante. / Reachability analysis is part of model checking. It consists to model complex systems by three sets : initial language, unwanted configurations and rewrite system. The initial language and the unwanted configurations language are sets of terms. Terms are words which are construct with symbols that have an arity that can be greater than 1. The rewrite system represent the dynamic of the complex system. It is a set of rules that permit from a initial term to obtain a new term. One of the approaches to analyze reachability from this modelling is to compute the set of reachable configurations. This set which is called set of descendants is obtained by applying the rewrite system on the initial language until obtaining no more new terms. After the set of descendants is computed, we need to compute the intersection between this set and the unwanted configurations set. If this intersection is empty then there is no unwanted configuration reachable, else the configurations in this intersection are reachable. However, the set of descendants is not computable in the general case. To bypass this problem, we compute an over-approximation of descendants.Now, if the intersection is empty, we keep proving that no unwanted configuration is reachable. Nevertheless, if the intersection is not empty, it is not possible to know if it comes from false-positives or form unwanted reachable configurations. So, the precision of the over-approximation is decisive.

Dans le cadre de ce sujet de thèse, on s'intéresse à la surveillance des systèmes hybrides à forte dynamique événementielle. L'objectif est de détecter les défauts permanents et intermittents qui causent l'accélération et le ralentissement des tâches des systèmes. C'est dans ce contexte que se situent les principales contributions suivantes des travaux consignés dans la présente thèse : - Le développement d'une méthode de surveillance des processus basée sur les automates hybrides linéaires (AHL). Cette méthode consiste en premier lieu à l'établissement du modèle AHL du système dynamique en tenant compte des contraintes physiques et dynamiques de celui-ci. - La réalisation d'une analyse d'atteignabilité qui consiste à définir toutes les trajectoires pouvant amener le système à son objectif tout en respectant le cahier des charges qui lui est imposé. L'extension de l'approche en utilisant les automates hybrides rectangulaires. Cette sous-classe d'automates nous a permis de modéliser des systèmes plus complexes donc une modélisation hybride riche et a permis également une analyse formelle. Cette partie a été ponctuée par l'implémentation du système de surveillance qui consiste à déterminer les équations caractérisant chaque sommet de l'automate qui modélise le système. / As part of this thesis, we focus on the monitoring of hybrid systems with high dynamic event. The aim is to detect faults that cause permanent and intermittent acceleration and deceleration systems tasks. It is in this context that the following are the main contributions of the work reported in this thesis: - The development of a method for process monitoring based on linear hybrid automata (AHL). This method involves first the establishment of the AHL model the dynamic system taking into account the physical and dynamic one. - The realization of a reachability analysis of defining all paths that can cause the system to its target while respecting the specifications imposed on it. The extension of the approach using the rectangular hybrid automata. This class of controllers has allowed us to model more complex systems, therefore, a hybrid modeling rich and also allowed a formal analysis. This part was punctuated by the implementation of the monitoring system by determining equations characterizing each summit of the automaton that models the system.

This work is concerned with analysing the potential impact of direct changes to large- scale enterprise systems, and, in particular, how to minimise testing efforts on such changes. A typical enterprise system may consist of hundreds of thousands of classes and millions of methods. Thus, it is extremely costly and difficult to apply conventional testing techniques to such a system. Retesting everything after a change is very expensive, and in practice generally not necessary. Selective testing can be more effective. However, it requires a deep understanding of the target system and a lack of that understanding can lead to insufficient test coverage. Change Impact Analysis can be used to estimate the impacts of the changes to be applied, providing developers/testers with confidence in selecting necessary tests and identifying untested entities. Conventional change impact analysis approaches include static analysis, dynamic analysis or a hybrid of the two analyses. They have proved to be useful on small or medium size programs, providing users an inside view of the system within an acceptable running time. However, when it comes to large-scale enterprise systems, the sizes of the programs are orders of magnitude larger. Conventional approaches often run into resource problems such as insufficient memory and/or unacceptable running time (up to weeks). More critically, a large number of false-negatives and false-positives can be generated from those approaches.In this work, a conservative static analysis with the capability of dealing with inheritance was conducted on an enterprise system and associated changes to obtain all the potential impacts. Later an aspect-based dynamic analysis was used to instrument the system and collect a set of dynamic impacts at run-time. We are careful not to discard impacts unless we can show that they are definitely not impacted by the change. Reachability analysis examines the program to see “Whether a given path in a program representation corresponds to a possible execution path”. In other words, we employ reachability analysis to eliminate infeasible paths (i.e., miss-matched calls and returns) that are identified in the control-flow of the program. Furthermore, in the phase of alias analysis, we aim at identifying paths that are feasible but cannot be affected by the direct changes to the system, by searching a set of possible pairs of accesses that may be aliased at each program point of interest. Our contributions are, we designed a hybrid approach that combines static anal- ysis and dynamic analysis with reachability analysis and alias/pointer analysis, it can be used to (1) solve the scalability problem on large-scale systems, (2) reduce false-positives and not introduce false-negatives, (3) extract both direct and indirect changes, and (4) identify impacts even before making the changes. Using our approach, organizations can focus on a much smaller, relevant subset of the overall test suite instead of blindly doing their entire suite of tests. Also it enables testers to augment the test suite with tests applying to uncovered impacts. We include an empirical study that illustrates the savings that can be attained. / Thesis / Doctor of Philosophy (PhD)

Many chemical engineering applications, such as safety verification and parameter estimation, require global optimization of dynamic models. Global optimization algorithms typically require obtaining global bounding information of the dynamic system, to aid in locating and verifying the global optimum. The typical approach for providing these bounds is to generate convex relaxations of the dynamic system and minimize them using a local optimization solver. Tighter convex relaxations typically lead to tighter lower bounds, so that the number of iterations in global optimization algorithms can be reduced. To carry out this local optimization efficiently, subgradient-based solvers require gradients or subgradients to be furnished. Smooth convex relaxations would aid local optimization even more. To address these issues and improve the computational performance of global dynamic optimization, this thesis proposes several novel formulations for constructing tight convex relaxations of dynamic systems. In some cases, these relaxations are smooth. Firstly, a new strategy is developed to generate convex relaxations of implicit functions, under minimal assumptions. These convex relaxations are described by parametric programs whose constraints are convex relaxations of the residual function. Compared with established methods for relaxing implicit functions, this new approach does not assume uniqueness of the implicit function and does not require the original residual function to be factorable. This new strategy was demonstrated to construct tighter convex relaxations in multiple numerical examples. Moreover, this new convex relaxation strategy extends to inverse functions, feasible-set mappings in constraint satisfaction problems, as well as parametric ordinary differential equations (ODEs). Using a proof-of-concept implementation in Julia, numerical examples are presented to illustrate the convex relaxations produced for various implicit functions and optimal-value functions. In certain cases, these convex relaxations are tighter than those generated with existing methods. Secondly, a novel optimization-based framework is introduced for computing time-varying interval bounds for ODEs. Such interval bounds are useful for constructing convex relaxations of ODEs, and tighter interval bounds typically translate into tighter convex relaxations. This framework includes several established bounding approaches, but also includes many new approaches. Some of these new methods can generate tighter interval bounds than established methods, which are potentially helpful for constructing tighter convex relaxations of ODEs. Several of these approaches have been implemented in Julia. Thirdly, a new approach is developed to improve a state-of-the-art ODE relaxation method and generate tighter and smooth convex relaxations. Unlike state-of-the-art methods, the auxiliary ODEs used in these new methods for computing convex relaxations have continuous right-hand side functions. Such continuity not only makes the new methods easier to implement, but also permits the evaluation of the subgradients of convex relaxations. Under some additional assumptions, differentiable convex relaxations can be constructed. Besides that, it is demonstrated that the new convex relaxations are at least as tight as state-of-the-art methods, which benefits global dynamic optimization. This approach has been implemented in Julia, and numerical examples are presented. Lastly, a new approach is proposed for generating a guaranteed lower bound for the optimal solution value of a nonconvex optimal control problem (OCP). This lower bound is obtained by constructing a relaxed convex OCP that satisfies the sufficient optimality conditions of Pontryagin's Minimum Principle. Such lower bounding information is useful for optimizing the original nonconvex OCP to a global minimum using deterministic global optimization algorithms. Compared with established methods for underestimating nonconvex OCPs, this new approach constructs tighter lower bounds. Moreover, since it does not involve any numerical approximation of the control and state trajectories, it provides lower bounds that are reliable and consistent. This approach has been implemented for control-affine systems, and numerical examples are presented. / Thesis / Doctor of Philosophy (PhD)

Computational biology and bioinformatics for apoptosis have been gaining much momentum due to the advances in computational sciences. Both fields use extensive computational techniques and modeling to mimic real world behaviors. One problem of particular interest is on the study of reachability, in which the goal is to determine if a target state or protein concentration in the model is realizable for a signaling pathway. Another interesting problem is to examine faulty pathways and how a fault can make a previously unrealizable state possible, or vice versa. Such analysis can be extremely valuable to the understanding of apoptosis. However, these analyses can be costly or even impractical for some approaches, since they must simulate every aspect of the model. Our approach introduces an abstracted model to represent a portion of the apoptosis signaling pathways as a finite state machine. This abstraction allows us to apply hardware testing and verification techniques and also study the behaviors of the system without full simulation. We proposed a framework that is tailor-built to implement these verification techniques for the discrete model. Through solving Boolean constraint satisfaction problems (SAT-based) and with guided stimulation (Genetic Algorithm), we can further extract the properties and behaviors of the system. Furthermore, our model allows us to conduct cause-effect analysis of the apoptosis signaling pathways. By constructing single- and double-fault models, we are able to study what fault(s) can cause the model to malfunction and the reasons behind it. Unlike simulation, our abstraction approach allows us to study the system properties and system manipulations from a different perspective without fully relying on simulation. Using these observations as hypotheses, we aim to conduct laboratory experiments and further refine our model. / Master of Science

La conception d'architectures opérationnelles d'un système de contrôle-commande est une phase très importante lors de la conception de systèmes de production d'énergie. Cette phase consiste à projeter l'architecture fonctionnelle sur l'architecture organique tout en respectant des contraintes de capacité et de sûreté, c'est-à-dire à allouer les fonctions de commande à un ensemble de contrôleurs tout en respectant ces contraintes. Les travaux présentés dans cette thèse proposent : i)une formalisation des données et contraintes du problème d'allocation de fonctions - ii)une méthode d'allocation, par recherche d'atteignabilité, basée sur un mécanisme d'appel/réponse dans un réseau d'automates communicants à variables entières - iii)la comparaison de cette méthode à une méthode de résolution par programmation linéaire en nombres entiers. Les résultats de ces travaux ont été validés sur des exemples de taille réelle et ouvrent la voie à des couplages entre recherche d'atteignabilité et programmation linéaire en nombres entiers pour la résolution de problèmes de satisfaction de systèmes de contraintes non linéaires. / The design of operational control architectures is a very important step of the design of energy production systems. This step consists in mapping the functional architecture of the system onto its hardware architecture while respecting capacity and safety constraints, i.e. in allocating control functions to a set of controllers while respecting these constraints. The work presented in this thesis presents: i) a formalization of the data and constraints of the function allocation problem- ii) a mapping method, by reachability analysis, based on a request/response mechanism in a network of communicating automata with integer variables- iii) a comparison between this method and a resolution method by integer linear programming. The results of this work have been validated on examples of actual size and open the way to the coupling between reachability analysis and integer linear programming for the resolution of satisfaction problems for non-linear constraint systems.

Planejamento em inteligência artificial é a tarefa de determinar ações que satisfaçam um dado objetivo. Nos problemas de planejamento sob incerteza, as ações podem ter efeitos probabilísticos. Esses problemas são modelados como Processos de Decisão Markovianos (Markov Decision Processes - MDPs), modelos que permitem o cálculo de soluções ótimas considerando o valor esperado de cada ação em cada estado. Contudo, resolver problemas grandes de planejamento probabilístico, i.e., com um grande número de estados e ações, é um enorme desafio. MDPs grandes podem ser reduzidos através da computação de bissimulações estocásticas, i.e., relações de equivalência sobre o conjunto de estados do MDP original. A partir das bissimulações estocásticas, que podem ser exatas ou aproximadas, é possível obter um modelo abstrato reduzido que pode ser mais fácil de resolver do que o MDP original. No entanto, para problemas de alguns domínios, a computação da bissimulação estocástica sobre todo o espaço de estados é inviável. Os algoritmos propostos neste trabalho estendem os algoritmos usados para a computação de bissimulações estocásticas para MDPs de forma que elas sejam computadas sobre o conjunto de estados alcançáveis a partir de um dado estado inicial, que pode ser muito menor do que o conjunto de estados completo. Os resultados experimentais mostram que é possível resolver problemas grandes de planejamento probabilístico com desempenho superior às técnicas conhecidas de bissimulação estocástica. / Planning in artificial intelligence is the task of finding actions to reach a given goal. In planning under uncertainty, the actions can have probabilistic effects. This problems are modeled using Markov Decision Processes (MDPs), models that enable the computation of optimal solutions considering the expected value of each action when applied in each state. However, to solve big probabilistic planning problems, i.e., those with a large number of states and actions, is still a challenge. Large MDPs can be reduced by computing stochastic bisimulations, i.e., equivalence relations over the original MDP states. From the stochastic bisimulations, that can be exact or approximated, it is possible to get an abstract reduced model that can be easier to solve than the original MDP. But, for some problems, the stochastic bisimulation computation over the whole state space is unfeasible. The algorithms proposed in this work extend the algorithms that are used to compute stochastic bisimulations for MDPs in a way that they can be computed over the reachable set of states with a given initial state, which can be much smaller than the complete set of states. The empirical results show that it is possible to solve large probabilistic planning problems with better performance than the known techniques of stochastic bisimulation.

This thesis presents a framework to verify asynchronous real-time systems based on model checking. These systems are modeled by using a common modeling formalism named Labeled Petri-nets(LPNs). In order to verify the real-time systems algorithmically, the zone-based timing analysis method is used for LPNs. It searches the state space with timing information (represented by zones). When there is a high degree of concurrency in the model, firing concurrent enabled transitions in different order may result in different zones, and these zones may be combined without affecting the verification result. Since the zone-based method could not deal with this problem efficiently, the POSET timing analysis method is adopted for LPNs. It separates concurrency from causality and generates an exactly one zone for a single state. But it needs to maintain an extra POSET matrix for each state. In order to save time and memory, an improved zone-based timing analysis method is introduced by integrating above two methods. It searches the state space with zones but eliminates the use of the POSET matrix, which generates the same result as with the POSET method. To illustrate these methods, a circuit example is used throughout the thesis. Since the state space generated is usually very large, a graph data structure named multi-value decision diagrams (MDDs) is implemented to store the zones compactly. In order to share common clock value of dierent zones, two zone encoding methods are described: direct encoding and minimal constraint encoding. They ignore the unnecessary information in zones thus reduce the length of the integer tuples. The effectiveness of these two encoding methods is demonstrated by experimental result of the circuit example.

The problem of analyzing concurrent systems has been investigated by many researchers, and several solutions have been proposed. Among the proposed techniques, reachability analysis—systematic enumeration of reachable states in a finite-state model—is attractive because it is conceptually simple and relatively straightforward to automate and can be used in conjunction with model-checking procedures to check for application-specific as well as general properties. The system validation problem considered here is the problem of verifying that the original specification is itself logically consistent. If, for instance, the specification has a design error, an implementation is expected to pass a conformance test if it contains the same error. A validation for the logical consistency of the system, however, must reveal the design error. An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually. This type of validation is traditionally performed by the symbolic execution of a finite state machine model of the system studied. The author presents an overview of the existing validation techniques and methods. Specified and analyzed systems are presented as reachable state graph. The implementation of the aggregate specifications validation system is also presented.