Many hours are spent by systemand control engineers deriving reduced order dynamicmodels portraying the dominant systemdynamics of thermohydraulic systems. A need therefore exists to develop a method that will automate the model derivation process. The model format preferred for control system design and analysis during preliminary system design is the state space format. The aim of this study is therefore to develop an automated and generic state space model extraction method that can be applied to thermohydraulic systems. Well developed system identification methods exist for obtaining state space models from input-output data, but these models are not transparent, meaning the parameters do not have any physical meaning. For example one cannot identify system parameters such as heat or mass transfer coefficients. Another approach is needed to derive state space models automatically. Many commercial thermohydraulic simulation codes follow a network approach towards the representation of thermohydraulic systems. This approach is probably one of the most advanced approaches in terms of technical development. It would therefore be useful to develop a state space extraction algorithm that would be able to derive reduced order state space models from network representations of thermohydraulic systems. In this regard a network approach is followed in the development of the state space extraction algorithm. The advantage of using a network-based extraction method is that the extracted state space model is transparent and the algorithm can be embedded in existing simulation software that follow a network approach. In this study an existing state space extraction algorithm, used for electrical network analysis, is modified and applied in a new way to extract state space models of thermohydraulic systems. A thermohydraulic system is partitioned into its respective physical domains which, unlike electrical systems, have multiple variables. Network representations are derived for each domain. The state space algorithm is applied to these network representations to extract symbolic state spacemodels. The symbolic parametersmay then be substitutedwith numerical values. The state space extraction algorithm is applied to small scale thermohydraulic systems such as a U-tube and a heat exchanger, but also to a larger, more complex system such as the Pebble Bed Modular Reactor Power Conversion Unit (PBMR PCU). It is also shown that the algorithm can extract linear, nonlinear, time-varying and time-invariant state space models. The extracted state space models are validated by solving the state space models and comparing the solutions with Flownex results. Flownex is an advanced and extensively validated thermo-fluid simulation code. The state space models compared well with Flownex results. The usefulness of the state space model extraction algorithm in model-based control system design is illustrated by extracting a linear time-invariant state space model of the PBMR PCU. This model is embedded in an optimal model-based control scheme called Model-Predictive Control (MPC). The controller is compared with standard optimised control schemes such as PID and Fuzzy PID control. The MPC controller shows superior performance compared to these control schemes. This study succeeded in developing an automated state space model extraction method that can be applied to thermohydraulic networks. Hours spent on writing down equations from first principles to derive reduced order models for control purposes can now be replaced with a click of a button. The need for an automated state space model extraction method for thermohydraulic systems has therefore been resolved / Thesis (Ph.D. (Computer and Electronical Engineering)--North-West University, Potchefstroom Campus, 2009.

Many hours are spent by systemand control engineers deriving reduced order dynamicmodels portraying the dominant systemdynamics of thermohydraulic systems. A need therefore exists to develop a method that will automate the model derivation process. The model format preferred for control system design and analysis during preliminary system design is the state space format. The aim of this study is therefore to develop an automated and generic state space model extraction method that can be applied to thermohydraulic systems. Well developed system identification methods exist for obtaining state space models from input-output data, but these models are not transparent, meaning the parameters do not have any physical meaning. For example one cannot identify system parameters such as heat or mass transfer coefficients. Another approach is needed to derive state space models automatically. Many commercial thermohydraulic simulation codes follow a network approach towards the representation of thermohydraulic systems. This approach is probably one of the most advanced approaches in terms of technical development. It would therefore be useful to develop a state space extraction algorithm that would be able to derive reduced order state space models from network representations of thermohydraulic systems. In this regard a network approach is followed in the development of the state space extraction algorithm. The advantage of using a network-based extraction method is that the extracted state space model is transparent and the algorithm can be embedded in existing simulation software that follow a network approach. In this study an existing state space extraction algorithm, used for electrical network analysis, is modified and applied in a new way to extract state space models of thermohydraulic systems. A thermohydraulic system is partitioned into its respective physical domains which, unlike electrical systems, have multiple variables. Network representations are derived for each domain. The state space algorithm is applied to these network representations to extract symbolic state spacemodels. The symbolic parametersmay then be substitutedwith numerical values. The state space extraction algorithm is applied to small scale thermohydraulic systems such as a U-tube and a heat exchanger, but also to a larger, more complex system such as the Pebble Bed Modular Reactor Power Conversion Unit (PBMR PCU). It is also shown that the algorithm can extract linear, nonlinear, time-varying and time-invariant state space models. The extracted state space models are validated by solving the state space models and comparing the solutions with Flownex results. Flownex is an advanced and extensively validated thermo-fluid simulation code. The state space models compared well with Flownex results. The usefulness of the state space model extraction algorithm in model-based control system design is illustrated by extracting a linear time-invariant state space model of the PBMR PCU. This model is embedded in an optimal model-based control scheme called Model-Predictive Control (MPC). The controller is compared with standard optimised control schemes such as PID and Fuzzy PID control. The MPC controller shows superior performance compared to these control schemes. This study succeeded in developing an automated state space model extraction method that can be applied to thermohydraulic networks. Hours spent on writing down equations from first principles to derive reduced order models for control purposes can now be replaced with a click of a button. The need for an automated state space model extraction method for thermohydraulic systems has therefore been resolved / Thesis (Ph.D. (Computer and Electronical Engineering)--North-West University, Potchefstroom Campus, 2009.

This dissertation presents two kinds of model extraction approaches, direct extraction and adaptive rational approximation methods, for establishing a novel broadband model, the modified T-equivalent circuit. Both methods skillfully use the simplified and decomposed schemes to dramatically reduce the complexity of modeled parameter extraction procedures and the needed computational efforts. As a result, any two-port microwave passive components or networks can be modeled efficiently using the proposed fully-analytical mathematic extraction formulations. In comparison with other broadband modeling techniques, the modified T-equivalent circuit can be constructed with much less elements. Model with such a compact character attributes the frequency responses of two decomposed circuits having obvious resonances to be identified and utilized for constituting equivalent circuits using only necessary elements. It is worth to note that the modified T-equivalent circuit model can utilize two expandable multilayer resonators to achieve very wide bandwidth but maintain model still in a single-stage equivalent circuit. Several successful modeling examples verified on the LTCC- and organic- embedded type of band-pass filters and inductors, the most crucial passive components to affect the performances of RF communication system, demonstrate the presented model with the superior character of accuracy and broadband indeed.

The thesis proposes a hybrid broadband equivalent model extraction method, and our goal is to combine via structure and irregular transmission line in print circuit board for extraction of broadband SPICE-compatible model by using the time domain algorithm and full wave simulation in frequency domain, respectively. We can construct broadband SPICE-compatible macro-model scalable library with two kind of different extraction methods, tow kind of extraction of equivalent model can construct the circuit structure for designer demand. Every modules of the broadband macro model of the two extraction models are represented by the optimum pole-residue forms. Using a systematic lumped-model extraction technique, all the optimum pole-residue rational functions can be transfered into a corresponding lumped circuit model. The accuracy of Extraction of Broadband Equivalent Models is demonstrated in frequency -domain responses compared with the 3D-FDTD or HFSS simulation. In addition, the extraction model can simulate in commercial tools effectively, ex: Hspice¡BADS. Even the model can simulate signal integrality and power integrality in Hspice or ADS.

Deep Neural Networks (DNNs) have become ubiquitous due to their performance on prediction and classification problems. However, they face a variety of threats as their usage spreads. Model extraction attacks, which steal DNN models, endanger intellectual property, data privacy, and security. Previous research has shown that system-level side channels can be used to leak the architecture of a victim DNN, exacerbating these risks. We propose a novel DNN architecture extraction attack, called EZClone, which uses aggregate rather than time-series GPU profiles as a side-channel to predict DNN architecture. This approach is not only simpler, but also requires less adversary capability than earlier works. We investigate the effectiveness of EZClone under various scenarios including reduction of attack complexity, against pruned models, and across GPUs with varied resources. We find that EZClone correctly predicts DNN architectures for the entire set of PyTorch vision architectures with 100\% accuracy. No other work has shown this degree of architecture prediction accuracy with the same adversarial constraints or using aggregate side-channel information. Prior work has shown that, once a DNN has been successfully cloned, further attacks such as model evasion or model inversion can be accelerated significantly. Then, we evaluate several mitigation techniques against EZClone, showing that carefully inserted dummy computation reduces the success rate of the attack.

Many organizations turn to the promise of artificial intelligence and machine learning (ML) as its use gains traction in many disciplines. However, developing high-performing ML models is often expensive. The design work can be complicated. Collecting large training datasets is often costly and can contain sensitive or proprietary information. For many reasons, machine learning models make for an appetizing target to an adversary interested in stealing data, model properties, or model behavior.  This work explores model extraction attacks and aims at designing an approximation-based monitor for tracking the progress of a potential adversary. When triggered, action can be taken to address the threat. The proposed monitor utilizes the interaction with a targeted model, continuously training a monitor model as a proxy for what the attacker could achieve, given the data gathered from the target.  The usefulness of the proposed monitoring approach is shown for two experimental attack scenarios. One explores the use of parametric and Bayesian models for a regression case, while the other explores commonly used neural network architectures for image classification.  The experiments expand current monitoring research to include ridge regression, Gaussian process regression, and a set of standard variants of convolutional neural networks: ResNet, VGG, and DenseNet. It also explores model and dataset similarity using metrics from statistical analysis, linear algebra, optimal transport, and a rank score. / Många organisationer vänder sig till löftet om artificiell intelligens och maskininlärning (ML) då dess användning vinner mark inom allt fler discipliner. Att utveckla högpresterande ML-modeller är dock ofta kostsamt. Designarbetet kan vara komplicerat. Att samla in stora träningsdataset är ofta dyrt och kan innehålla känslig eller proprietär information. Det finns många skäl till att maskininlärningsmodeller kan vara lockande mål för en motståndare som är ute efter att stjäla data, modellparametrar eller modellbeteende. Det här arbetet utforskar modellextraktionsattacker och syftar till att utforma en approximationsbaserad monitorering som följer framstegen för en potentiell motståndare. När en attack är konstaterad kan åtgärder vidtas för att hantera hotet. Den föreslagna monitorn utnyttjar interaktionen med målmodellen. Den tränar kontinuerligt en monitor-modell som en fungerar som en approximation för vad angriparen skulle kunna uppnå med de data som samlats in från målmodellen. Nyttan av den föreslagna övervakningsansatsen visas för två experimentella attackscenarier. Det ena utforskar användningen av parametriska och Bayesianska modeller för ett regressionsfall, medan det andra utforskar vanligt använda neurala nätverksarkitekturer för ett bildklassificeringsfall. Experimenten utvidgar aktuell forskning kring monitorer till att att inkludera Ridge regression, Gauassian process regression och en uppsättning standardvarianter av convolutional neural networks: ResNet, VGG och DenseNet. Experimenten utforskar även likhet mellan ML-modeller och dataset med hjälp av mått från statistisk analys, linjär algebra, optimal transport samt rangapproximation.

Thesis (MSc)--University of Stellenbosch, 2003. / ENGLISH ABSTRACT: Model checking is a computer-aided verification technique that is used to verify properties about the formal description of a system automatically. This technique has been applied successfully to detect subtle errors in reactive systems. Such errors are extremely difficult to detect by using traditional testing techniques. The conventional method of applying model checking is to construct a model manually either before or after the implementation of a system. Constructing such a model requires time, skill and experience. An alternative method is to derive a model from an implementation automatically. In this thesis two techniques of applying model checking to reactive systems are compared, both of which have problems as well as advantages. Two specific strategies are compared in the area of protocol development: 1. Structuring a protocol as a transition system, modelling the system, and then deriving an implementation from the model. 2. Automatically translating implementation code to a verifiable model. Structuring a reactive system as a transition system makes it possible to verify the control flow of the system at implementation level-as opposed to verifying the control flow at abstract level. The result is a closer correspondence between implementation and specification (model). At the same time testing, which is restricted to small, independent code fragments that manipulate data, is simplified significantly. The construction of a model often takes too long; therefore, verification results may no longer be applicable when they become available. To address this problem, the technique of automated model extraction was suggested. This technique aims to reduce the time required to construct a model by minimising manual input during model construction. A transition system is a low-level formalism and direct execution through interpretation is feasible. However, the overhead of interpretation is the major disadvantage of this technique. With automated model extraction there are disadvantages too. For example, differences between the implementation and specification languages-such as constructs present in the implementation language that cannot be expressed in the modelling language-make the development of an automated model extraction tool extremely difficult. In conclusion, the two techniques are compared against a set of software development considerations. Since a specific technique is not always preferable, guidelines are proposed to help select the best approach in different circumstances. / AFRIKAANSE OPSOMMING: Modeltoetsing is 'n rekenaargebaseerde verifikasietegniek wat gebruik word om eienskappe rakende 'n formele spesifikasie van 'n stelsel te verifieer. Die tegniek is al suksesvol toegepas om subtiele foute in reaktiewe stelsels op te spoor. Sulke foute word uiters moeilik opgespoor as tradisionele toetsings tegnieke gebruik word. Tradisioneel word modeltoetsing toegepas deur 'n model te bou voor of na die implementasie van 'n stelsel. Om'n model te bou verg tyd, vernuf en ervaring. 'n Alternatiewe metode is om outomaties 'n model van 'n implementasie af te lei. In hierdie tesis word twee toepassingstegnieke van modeltoetsing vergelyk, waar beide tegnieke beskik oor voordele sowel as nadele. Twee strategieë word vergelyk in die gebied van protokol ontwikkeling: 1. Om 'n protokol as 'n oorgangsstelsel te struktureer, dit te moduleer en dan 'n implementasie van die model af te lei. 2. Om outomaties 'n verifieerbare model van 'n implementasie af te lei. Om 'n reaktiewe stelsel as 'n oorgangsstelsel te struktureer maak dit moontlik om die kontrolevloei op implementasie vlak te verifieer-in teenstelling met verifikasie van kontrolevloei op 'n abstrakte vlak. Die resultaat is 'n nouer band wat bestaan tussen die implementasie en die spesifikasie. Terselfdetyd word toetsing, wat beperk word tot klein, onafhanklike kodesegmente wat data manupileer, beduidend vereenvoudig. Die konstruksie van 'n model neem soms te lank; gevolglik, wanneer die verifikasieresultate beskikbaar word, is dit dalk nie meer toepaslik op die huidige weergawe van 'n implementasie nie. Om die probleem aan te spreek is 'n tegniek om modelle outomaties van implementasies af te lei, voorgestel. Die doel van die tegniek is om die tyd wat dit neem om 'n model te bou te verminder deur handtoevoer tot 'n minimum te beperk. 'n Oorgangsstelsel is 'n laevlak formalisme en direkte uitvoering deur interpretasie is wesenlik. Die oorhoofse koste van die interpreteerder is egter die grootste nadeel van die tegniek. Daar is ook nadele wat oorweeg moet word rakende die tegniek om outomaties modelle van implementasies af te lei. Byvoorbeeld, verskille tussen die implementasietaal en spesifikasietaal=-soos byvoorbleed konstrukte wat in die implementasietaal gebruik word wat nie in die modeleringstaal voorgestel kan word nie-vrnaak die ontwikkeling van 'n modelafieier uiters moeilik. As gevolg word die twee tegnieke vergelyk teen 'n stel van programatuurontwikkelingsoorwegings. Omdat 'n spesifieke tegniek nie altyd voorkeur kan geniet nie, word riglyne voorgestel om te help met die keuse om die beste tegniek te kies in verskillende omstandighede.

Conversion of discrete volumetric data to boundary representation is quite common operation. Standard approach to resolve this problem is to use well-known Marching cubes algorithm, which although simple and robust, generates low-quality output that requires subsequent post-processing. This master's thesis deals with uncommon algorithms used for isosurface extraction from volumes. The reader will be acquainted with fundamental principles of Hierarchical Iso-Surface Extraction method, that was independently implemented and tested in this work.

Cars, trains, trucks, telecom networks and industrial robots are examples of products relying on complex embedded software systems, running on embedded computers. Such systems may consist of millions of lines of program code developed by hundreds of engineers over many years, often decades. Over the long life-cycle of such systems, the main part of the product development costs is typically not the initial development, but the software maintenance, i.e., improvements and corrections of defects, over the years. Of the maintenance costs, a major cost is the verification of the system after changes has been applied, which often requires a huge amount of testing. However, today's techniques are not sufficient, as defects often are found post-release, by the customers. This area is therefore of high relevance for industry. Complex embedded systems often control machinery where timing is crucial for accuracy and safety. Such systems therefore have important requirements on timing, such as maximum response times. However, when maintaining complex embedded software systems, it is difficult to predict how changes may impact the system's run-time behavior and timing, e.g., response times.Analytical and formal methods for timing analysis exist, but are often hard to apply in practice on complex embedded systems, for several reasons. As a result, the industrial practice in deciding the suitability of a proposed change, with respect to its run-time impact, is to rely on the subjective judgment of experienced developers and architects. This is a risky and inefficient, trial-and-error approach, which may waste large amounts of person-hours on implementing unsuitable software designs, with potential timing- or performance problems. This can generally not be detected at all until late stages of testing, when the updated software system can be tested on system level, under realistic conditions. Even then, it is easy to miss such problems. If products are released containing software with latent timing errors, it may cause huge costs, such as car recalls, or even accidents. Even when such problems are found using testing, they necessitate design changes late in the development project, which cause delays and increases the costs. This thesis presents an approach for impact analysis with respect to run-time behavior such as timing and performance for complex embedded systems. The impact analysis is performed through optimizing simulation, where the simulation models are automatically generated from the system implementation. This approach allows for predicting the consequences of proposed designs, for new or modified features, by prototyping the change in the simulation model on a high level of abstraction, e.g., by increasing the execution time for a particular task. Thereby, designs leading to timing-, performance-, or resource usage problems can be identified early, before implementation, and a late redesigns are thereby avoided, which improves development efficiency and predictability, as well as software quality. The contributions presented in this thesis is within four areas related to simulation-based analysis of complex embedded systems: (1) simulation and simulation optimization techniques, (2) automated model extraction of simulation models from source code, (3) methods for validation of such simulation models and (4) run-time recording techniques for model extraction, impact analysis and model validation purposes. Several tools has been developed during this work, of which two are in commercialization in the spin-off company Percepio AB. Note that the Katana approach, in area (2), is subject for a recent patent application - patent pending. / PROGRESS

Le développement de nouveaux formalismes logiques est au cœur de nombreuses problématiques de méthodes formelles. Ces formalismes doivent répondre à la fois à des impératifs de modélisation (ils doivent permettre de décrire certains systèmes) et de calcul (ils doivent fournir des méthodes de calcul correctes et complètes). Dans ce contexte, nous nous intéressons aux logiques de ressources, en particulier les logiques BI et BBI qui traitent du partage et de la séparation de ressources et qui ont conduit aux diverses logiques de séparation dont les applications à la vérification de programmes se sont développées fortement ces dernières années. Nous proposons dans cette thèse d’étudier, à partir des logiques BI et BBI, des logiques de séparation modales et épistémiques en se focalisant sur leurs capacités de modélisation et leur expressivité mais aussi les nouveaux calculs de preuve pour ces logiques. Une première étude a porté sur la modélisation de propriétés dynamiques de ressources au travers d’une nouvelle logique LTBI, qui est une logique de séparation temporelle, fondée sur la logique BI et des modalités temporelles. Cette logique offre notamment des perspectives intéressantes de modélisation temporelle branchante, permettant par exemple de caractériser les processus multi-thread. Une étude complémentaire a porté sur la modélisation de l’accès par des agents à des propriétés sous conditions de posséder certaines ressources, au travers d’une nouvelle logique ERL, qui est une logique de séparation épistémique, fondée sur la logique BBI et des modalités épistémiques. Cette logique permet de nombreuses modélisations de systèmes de contrôle d’accès. En vue d’étendre l’expressivité de telles logiques de séparation, comme la logique BBI et ses variantes, une étude sur l’internalisation des symboles de ressources dans la syntaxe de la logique a été développée au travers des nouvelles logiques HRL et HBBI (version hybride de BBI). L’internalisation permet à la fois d’étendre l’expressivité des logiques et d’axiomatiser la logique BBI et certaines de ses variantes. Outre la conception de ces logiques, l’étude de leur sémantique et aussi de leurs capacités de modélisation, une partie de cette thèse a été consacrée à la définition de calculs de preuve, ici de tableaux, pour ces nouvelles logiques ainsi qu’à leurs preuves de correction et de complétude / The design of new logical formalisms is at the heart of several problems in formal methods. Those formalisms must respond to requirements both concerning modelling (they must be able to describe certain systems) and computing (they must provide complete and sound calculus methods). In this context, we look at resource logics, and in particular BI and BBI logics, that deal with the separation and sharing of resources and have led to several separation logics whose applications to software verification have been widely developped recently. We propose in this thesis, starting from BI and BBI logics, to study some modal and epistemic separation logics by focusing on their modelling capacities and their expresiveness, as well as on the new proof calculi for those logics. A first study deals with the modelling of dynamic resource properties through new logic LTBI, which is a temporal separation logic, based on BI logic and temporal modalities. This logic notably offers interesting perspectives in temporal branching modelling, allowing for instance to characterize multi-thread processes. A complementary study concerns the modelling of access by agents to properties under the conditions of posessing some resources, through a new logic ERL, which is an epistemic separation logic, based on BBI logic and epistemic modalities. This logic allows many modellings of access control systems. In order to extend the expressivity of such separation logics, like BBI logic and its variants, a study on the internalization of resources symbols in the logic’s syntax has been developed through the new logics HRL and HBBI (hybrid version of BBI). Internalization allows both the extension of the expressivity of logics and the axiomatisation of BBI logic and some of its variants. In addition to the conception of those logics, the study of their semantics and their modelling capacities, a part of this thesis is dedicated to the definition of proof calculs, here tableaux calculus, for those new logics, as well as their proof of soundness and completeness