The present thrust in the electronics industry towards integrating multiple functions on a single chip while operating at very high frequencies has highlighted the need for efficient Electronic Design Automation (EDA) tools to shorten the design cycle and capture market windows. However, the increasing complexity in modern circuit design has made simulation a computationally cumbersome task. The notion of model order reduction has emerged as an effective tool to address this difficulty. Typically, there are numerous approaches and several issues involved in the implementation of model-order reduction techniques. Among the important ones of those issues is the problem of determining a suitable order (or size) for the reduced system. An optimal order would be the minimal order that enables the reduced system to capture the behavior of the original (more complex and larger) system up to a user-defined frequency. The contribution presented in this thesis describes a new approach aimed at determining the order of the reduced system. The proposed approach is based on approximating the impulse response of the original system in the time-domain. The core methodology in obtaining that approximation is based on numerically inverting the Laplace-domain of the representation of the impulse response from the complex-domain (s-domain) into the time-domain. The main advantage of the proposed approach is that it allows the order selection algorithm to operate directly on the time-domain form of the impulse response. It is well-known that numerically generating the impulse response in the time-domain is very difficult and its not impossible, since it requires driving the original network with the Dirac-delta function, which is a mathematical abstraction rather than a concrete waveform that can be implemented on a digital computer. However, such a difficulty is avoided in the proposed approach since it uses the Laplace-domain image of the impulse response to obtain its time-domain representation. The numerical simulations presented in the thesis demonstrate that using the time-domain waveform of the impulse response, computed using the proposed approach and properly filtered with a Butterworth filter, guides the order selection algorithm to select a smaller order, i.e., the reduced system becomes more compact in size. The phrase "smaller or more compact" in this context refers to the comparison with existing techniques currently in use, which seek to generate some form of time-domain approximations for the impulse response through driving the original network with pulse-shaped function (e.g., Gaussian pulse).

Dans le domaine de l'électrotechnique, la simulation numérique permet de s'affranchir d'essais qui peuvent être coûteux ou difficiles à réaliser. La Méthode des Éléments Finis est ainsi devenue une approche de référence dans ce contexte car elle permet d'obtenir des résultats précis sur des systèmes aux géométries complexes. Or, la simulation numérique d’un dispositif électrotechnique peut s’avérer coûteuse en temps de calcul du fait d’un nombre d’inconnues et de pas de temps important, ainsi que de fortes non-linéarités des matériaux ferromagnétiques. Il est alors nécessaire de mettre en œuvre des techniques permettant de réduire les temps de calcul nécessaires à la résolution de tels modèles numériques. Les méthodes de réduction de modèles semblent bien adaptées à ce type de problèmes car elles ont déjà été appliquées avec succès dans de nombreux domaines de l’ingénierie, notamment en mécanique des fluides et du solide. Une première catégorie de méthodes permet de rechercher la solution dans une base réduite afin de diminuer le nombre d’inconnues du modèle numérique. Pour ce type d’approche, les méthodes les plus connues sont la Proper Orthogonal Decomposition, la Proper Generalized Decomposition et la Projection d’Arnoldi. Une seconde catégorie regroupe les approches permettant de réduire le coût de calcul dû aux phénomènes non linéaires, grâce à des méthodes d’interpolation telles que l‘Empirical Interpolation Method et la Gappy POD. Cette thèse CIFRE a ainsi été effectuée dans le cadre du LAMEL (laboratoire commun entre le L2EP et EDF R&D) avec pour but d’identifier et d’implémenter les méthodes de réduction les mieux adaptées à l’électrotechnique. Celles-ci devront être capables de réduire le coût de calcul tout en prenant en compte le mouvement du rotor, les non-linéarités des matériaux ferromagnétiques mais aussi l’environnement électrique et mécanique du dispositif. Enfin, un indicateur évaluant l’erreur commise par le modèle réduit a été développé, offrant ainsi la garantie d’une précision suffisante sur les résultats. / In the electrical engineering field, numerical simulation allows to avoid experiments which can be expensive, difficult to carry out or harmful for the device. In this context, the Finite Element Method has become to be one of the most used approach since it allows to obtain precise results on devices with complex geometries. However, these simulations can be computationally expensive because of a large number of unknowns and time-steps, and of strong nonlinearities of ferromagnetic materials to take into account. Numerical techniques to reduce the computational effort are thus needed. In this context, model order reduction approaches seem well adapted to this kind of problem since they have already been successfully applied to many engineering fields, among others, fluid and solid mechanics. A first class of methods allows to seek the solution in a reduced basis, allowing to dramatically reduce the number of unknowns of the numerical model. The most famous technics are probably the Proper Orthogonal Decomposition, the Proper Generalized Decomposition and the Arnoldi Projection. The second class of approaches consists of methods allowing to reduce the computational cost associated to nonlinearities, using interpolation methods like the Empirical Interpolation Method and the Gappy POD. This Ph.D. has been done within the LAMEL, the joint laboratory between the L2EP and EDF R&D, in order to identify and implement the model order reduction methods which are the most adapted to electrical engineering models. These methods are expected to reduce the computational cost while taking into account the motion of an electrical machine rotor, the nonlinearities of the ferromagnetic materials and also the mechanical and electrical environment of the device. Finally, an error indicator which evaluates the error introduced by the reduction technic has been developed, in order to guarantee the accuracy of the results obtained with the reduced model.

京都大学 / 新制・課程博士 / 博士(工学) / 甲第23511号 / 工博第4923号 / 新制||工||1769(附属図書館) / 京都大学大学院工学研究科電気工学専攻 / (主査)教授 松尾 哲司, 教授 雨宮 尚之, 准教授 久門 尚史 / 学位規則第4条第1項該当 / Doctor of Philosophy (Engineering) / Kyoto University / DFAM

Large scale linear time invariant (LTI) systems arise in many physical and technical fields. An approximation, e.g. with model order reduction techniques, of this large systems is crucial for a cost efficient simulation. In this thesis we focus on a model order reduction method based on modal approximation, where the LTI system is projected onto the left and right eigenspaces corresponding to the dominant poles of the system. These dominant poles are related to the most dominant parts of the residue expansion of the transfer function and usually form a small subset of the eigenvalues of the system matrices. The computation of this dominant poles can be a formidable task, since they can lie anywhere inside the spectrum and the corresponding left eigenvectors have to be approximated as well. We investigate the subspace accelerated dominant pole algorithm and the two-sided and alternating Jacobi-Davidson method for this modal truncation approach. These methods can be seen as subspace accelerated versions of certain Rayleigh quotient iterations. Several strategies that admit an efficient computation of several dominant poles of single-input single-output LTI systems are examined. Since dominant poles can lie in the interior of the spectrum, we discuss also harmonic subspace extraction approaches which might improve the convergence of the methods. Extentions of the modal approximation approach and the applied eigenvalue solvers to multi-input multi-output are also examined. The discussed eigenvalue algorithms and the model order reduction approach will be tested for several practically relevant LTI systems.

La simulation numérique occupe une part de plus en plus importante dans les phases de conception mais aussi de validation de systèmes innovants. Dans le cadre de la conception d’une chaîne de traction d’un véhicule électrique, la simulation numérique peut par exemple être employée pour choisir une technologie de moteur électrique ou encore pour mettre au point des stratégies de pilotage au regard de critères de décision tels que l’autonomie du véhicule, son coût mais aussi sa performance.Les systèmes devenant de plus en plus complexes, ils requièrent des simulations de plus en plus fines afin d’appréhender au mieux les phénomènes qu’ils mettent en œuvre - par exemple l’étude des pertes fer dans une machine électrique. L’utilisation de simulations 3D permet d’avoir des résultats très précis à l’échelle d’un organe mais ne se prête pas encore aujourd’hui à l’étude de systèmes de grande taille (c’est-à-dire avec beaucoup de degrés de liberté, de nombreux paramètres d’optimisation et plusieurs domaines de la Physique en jeu). En effet, les simulations 3D sont d’autant plus coûteuses en temps de calcul que le modèle à étudier contient de degrés de liberté. C’est pourquoi, depuis quelques années les techniques de réduction de modèles attisent les développements. En effet, elles permettent de garantir un bon compromis entre le temps de calcul et la précision des résultats produits par les modèles réduits.Nous nous intéressons ici à l’utilisation de ces techniques dans un contexte industriel autour de deux axes : - l’étude de phénomènes thermiques (dans les modules d’électronique de puissance) - l’étude de phénomènes électromagnétiques (dans les machines électriques) / Numerical simulations are widely used during the design phase of a product but also for the validation of an innovative system. For example, during the conception of an electric vehicle’s powertrain, numerical simulations can be used to select the appropriate electric engine technology or for the development of control strategies taking into account decision criteria such as vehicle’s autonomy, but also its cost and performance.System’s complexity is always increasing, so they require more and more precise simulations in order to better understand the phenomena involved - for example to study iron losses in an electric engine. 3D simulations provide very accurate results to study a body but are still not appropriate today for the study of large scale systems (ie. with many degrees of freedom, many optimization parameters and several areas of Physics). Indeed, 3D simulations computing time cost is directly linked with the number of degrees of freedom. That’s why, in recent years, model order reduction techniques stir developments because they guarantee a good compromise between the computation time and accuracy of results produced by these models.In this study, we are interested in techniques that can be used in an industrial context around two axes: - the study of thermal phenomena (in the power electronics modules) - the study of electromagnetic phenomena (in electric engines)

Ce travail a été entrepris dans le cadre d’une coopération internationale entre l’Université de Brasilia, l’Agence spatiale brésilienne (AEB), l’ENS Paris-Saclay et le groupe SAFRAN. L’objet principal de cette coopération est l’étude du fretting-fatigue, problème de contact associé à des charges de fatigue qui réduisent considérablement la durée de vie des composants en raison de la concentration élevée de contraintes, de l’usure et des conditions de chargement non proportionnelles. En ce qui concerne les coûts de calcul élevés impliqués dans l’évaluation des applications industrielles, l’un des objectifs de ce travail est d’améliorer les performances des simulations de frettage utilisant une approche d’enrichissement. L'idée est de tirer parti du fait que les champs mécaniques autour des bords de contact dans des configurations de contact cylindriques dans des conditions de frottement sont similaires à ceux trouvés près du fond de fissure dans les problèmes de mécanique de rupture élastique linéaire. Cette similitude rend attrayante l’idée d’enrichir les simulations de frettage par éléments finis via le framework X-FEM, ce qui nous permet de travailler avec des maillages plus grossiers tout en conservant une bonne précision. Comme nous le montrerons dans ce travail, il est possible de travailler avec des maillages jusqu'à 10 fois plus grossiers que si une méthode par élements finis classique était utilisée, permettant une forte amélioration des performances de calcul.Ce travail étudiera également l’influence de la prise en compte des effets de l’usure dans la prévision de la durée de vie en fatigue. Par conséquent, des simulations par éléments finis du fretting-fatigue ont été effectuées en tenant compte de la mise à jour de la géométrie due à l'enlèvement de matière et les résultats ont été comparés aux données expérimentales et aux simulations par éléments finis dans lesquels les effets de l'usure ont été négligés (stratégie simplificatrice généralement adoptée pour évaluer les problèmes de fatigue de frottement). Les critères de fatigue multiaxiaux conventionnels associés à la théorie des distances critiques ont été utilisés pour prédire la vie. Les résultats ont montré que, pour les données évaluées ici, lorsque des essais de fretting-fatigue ont été menés sur un alliage Ti-6Al-4V dans des conditions de glissement partiel, considérer les effets de l'usure pourraient augmenter légèrement la précision des prévisions de durée de vie. Cependant, cette amélioration n’est peut-être pas digne d’intérêt si nous prenons en compte les coûts de calcul élevés dans les analyses d’usure. / This work has been undertaken in the context of an international research cooperation between the University of Brasilia, the Brazilian Space Agency (AEB), the ENS Paris-Saclay and the SAFRAN group. The main subject of this cooperation is the investigation of fretting fatigue, which is a contact problem in conjunction with fatigue loads responsible for reducing considerably components’ fatigue life due to the high stress concentration, wear and non-proportional loading conditions involved in such problems. Regarding the high computational costs involved when assessing industrial applications, one of the aims of this work is to improve the performance of fretting simulations making use of an enrichment approach. The idea is to take advantage of the fact that the mechanical fields around the contact edges in cylindrical contact configurations under fretting conditions are similar to the ones found close to the crack tip in linear elastic fracture mechanics problems. This similarity makes attractive the idea of enriching finite element fretting simulations through the X-FEM framework, which enables us to work with coarser meshes while keeping a good accuracy. As it will be shown in this work, it is possible to work with meshes up to 10 times coarser than it should be if a conventional FE method was used allowing a strong improvement of the computational performances.This work will also investigate the influence of considering wear effects in the prediction of fretting fatigue lives. Therefore, fretting fatigue FE simulations have been carried considering the geometry update due to the material removal and results were compared to both experimental data and FE simulations where wear effects were neglected (simplifying strategy usually adopted when evaluating fretting fatigue problems). Conventional multiaxial fatigue criteria in association with the Theory of Critical Distances have been used in order to predict life. Results have shown that, for the data here assessed, where fretting fatigue tests were conducted on a Ti-6Al-4V alloy under partial slip conditions, considering wear effects might slightly increase the accuracy of life predictions. However, this slight improvement may not be worthwhile regarding the increase in the computational cost when compared to standard approaches where wear is neglected.

No description available.

Gegenstand dieser Arbeit ist die Forschungsdisziplin, welche in der Strukturmechanik als Modellordnungsreduktion bekannt ist. Im Mittelpunkt stehen Kopplungsprozesse von starren und elastischen Mehrkörpersystemen - sowohl in theoretischer Hinsicht als auch bezüglich der praktischen Realisation im Rahmen des Finite-Elemente-Programms ANSYS und des Mehrkörpersimulationsprogramms SIMPACK. Eine Vielfalt von strukturerhaltendenMOR-Methoden wurde zum Zwecke des Überblicks dargestellt. Darüber hinaus findet sich eine Kategorisierungsmethodik in Hinsicht auf den später beschriebenen FEM-MKS-Kopplungsprozess. Die Effizienz der MOR-Methoden wird sowohl hinsichtlich der Qualität der ROM als auch bezogen auf die hierfür benötigte Rechenzeit bemessen. Aus diesem Grunde wurden etliche MOR Schemata dargelegt, mit dem Ziel, den Effizienzfaktor während der Berechnung eines ROMs zu maximieren, das heißt maximale Qualität und minimale Rechenzeit zu erzielen. Die Validierung der dynamischen ROM-Eigenschaften basiert auf der Anwendung der sogenannten Modellkorrelationskriterien. Dies wurde an vier Anwendungsbeispielen aus dem Feld der Strukturmechanik getestet: der 3D-Balkenstruktur, der UIC60-Schiene, dem Pleuel und der Kurbelwelle. Die Anwendung der diagonal perturbation-Methodik verbessert die Kondition der Steifigkeitsmatrix eines Modells, von beiden Arten von Lösungsprozeduren, d.h. direkte und iterative Verfahren, betroffen sind. Die dynamische Bewegung mechanischer MKS wird als ein Index-3-DAE-Systemformuliert und die Information über die elastischen Körper wird in Form der sogenannten Standard Input Datei in einen MKS-Code transferriert. Die Einführung des Back-projection-Ansatzes ermöglicht die weitere Verwendung bestimmter ROM-Typen, derren assoziierten physikalische Eigenschaften unangemessen definiert wurden. Zum Abschluss werden die theoretischen, modellierenden und numerischen Fortschritte der Arbeit resümiert und kombiniert im Sinne der Model Order Reduction Package Toolbox (MORPACK). Die Matlab-basierte MORPACK-Toolbox ermöglicht den FEM-MKS-Kopplungsprozess für die Verwendung von ANSYS und SIMPACK. Hierin sind ein Großteil der zuvor erläuterten Erweiterungen eingeschlossen. Mit Hilfe der zwei integrierten inneren MOR- und SID-Schnittstellen als auch der vier Anwendungsebenen wird der Import von freien oder eingespannten ROM in SIMPACK ermöglicht. / The research discipline referred to as the Model Order Reduction in structural mechanics is the topic of this Thesis. Special emphasis is given to the coupling process of rigid and elastic Multi Body Dynamics in terms of both the theoretical aspects and the practical realization within the environment of the commercial Finite Element and the Multi Body Systems software packages, ANSYS and SIMPACK respectively. In this regard, a variety of structure preserving Model Order Reduction methods is presented and a categorization methodology is provided in view of the later FEM-MBS coupling process. The algorithmic scheme of several of the MOR methods indicates the capability of generating qualitatively better Reduced Order Models than the standardized Guyan and Component Mode Synthesis approaches. The efficiency of a MOR method is measured in terms of both the quality of the ROM and the associated time required for the .computation Based on the application of the, so called, Model Correlation Criteria the efficiency of the MOR schemes is tested on four application examples originating from the area of structural mechanics, i.e. the 3D elastic solid bar structure, the UIC60 elastic rail, the elastic piston rod, and the elastic crankshaft model. Herewith, the superiority of alternative MOR schemes in comparison to Guyan or CMS methods is demonstrated in terms of the ROM?s quality and the computation time by the use of either the one-step or the two-step MOR algorithms. Numerous of the FE discretized structures suffer from the, so called, ill-conditioned properties regarding the associated stiffness matrix. On one hand, the direct solution of a MOR method might produce erroneous ROMs due to the associated truncation phenomenon and on the other hand, any kind of iterative approach suffers from vast computation times. The application of the diagonal perturbation methodology improves the condition properties of the model?s stiffness matrix and thus, both kinds of the aforementioned solution procedures are affected. The back-projection approach is introduced, which projects the ROM belonging to the Non physical subspace reduction-expansion methods category back onto the physical configuration space and thus, enabling its further usage in a MBS code, e.g. SIMPACK. Finally, the theoretical, modelling, and numerical advancements are combined in terms of the Model Order Reduction Package. The Matlab-based MORPACK toolbox enables the FEM-MBS coupling process for the ANSYS-SIMPACK utilization and herewith, several of the aforementioned enhancements are included. With the help of the two integrated inner interfaces, i.e. MOR and SID, as well as four application levels, the import into SIMPACK of alternatively free or fixed ROMs is enabled. The functionality of MORPACK is demonstrated based on two application examples, namely, the 3D elastic solid bar and the UIC60 elastic rail, the dynamic properties of which are validated prior to their import into SIMPACK.

Gegenstand dieser Arbeit ist die Forschungsdisziplin, welche in der Strukturmechanik als Modellordnungsreduktion bekannt ist. Im Mittelpunkt stehen Kopplungsprozesse von starren und elastischen Mehrkörpersystemen - sowohl in theoretischer Hinsicht als auch bezüglich der praktischen Realisation im Rahmen des Finite-Elemente-Programms ANSYS und des Mehrkörpersimulationsprogramms SIMPACK. Eine Vielfalt von strukturerhaltendenMOR-Methoden wurde zum Zwecke des Überblicks dargestellt. Darüber hinaus findet sich eine Kategorisierungsmethodik in Hinsicht auf den später beschriebenen FEM-MKS-Kopplungsprozess. Die Effizienz der MOR-Methoden wird sowohl hinsichtlich der Qualität der ROM als auch bezogen auf die hierfür benötigte Rechenzeit bemessen. Aus diesem Grunde wurden etliche MOR Schemata dargelegt, mit dem Ziel, den Effizienzfaktor während der Berechnung eines ROMs zu maximieren, das heißt maximale Qualität und minimale Rechenzeit zu erzielen. Die Validierung der dynamischen ROM-Eigenschaften basiert auf der Anwendung der sogenannten Modellkorrelationskriterien. Dies wurde an vier Anwendungsbeispielen aus dem Feld der Strukturmechanik getestet: der 3D-Balkenstruktur, der UIC60-Schiene, dem Pleuel und der Kurbelwelle. Die Anwendung der diagonal perturbation-Methodik verbessert die Kondition der Steifigkeitsmatrix eines Modells, von beiden Arten von Lösungsprozeduren, d.h. direkte und iterative Verfahren, betroffen sind. Die dynamische Bewegung mechanischer MKS wird als ein Index-3-DAE-Systemformuliert und die Information über die elastischen Körper wird in Form der sogenannten Standard Input Datei in einen MKS-Code transferriert. Die Einführung des Back-projection-Ansatzes ermöglicht die weitere Verwendung bestimmter ROM-Typen, derren assoziierten physikalische Eigenschaften unangemessen definiert wurden. Zum Abschluss werden die theoretischen, modellierenden und numerischen Fortschritte der Arbeit resümiert und kombiniert im Sinne der Model Order Reduction Package Toolbox (MORPACK). Die Matlab-basierte MORPACK-Toolbox ermöglicht den FEM-MKS-Kopplungsprozess für die Verwendung von ANSYS und SIMPACK. Hierin sind ein Großteil der zuvor erläuterten Erweiterungen eingeschlossen. Mit Hilfe der zwei integrierten inneren MOR- und SID-Schnittstellen als auch der vier Anwendungsebenen wird der Import von freien oder eingespannten ROM in SIMPACK ermöglicht. / The research discipline referred to as the Model Order Reduction in structural mechanics is the topic of this Thesis. Special emphasis is given to the coupling process of rigid and elastic Multi Body Dynamics in terms of both the theoretical aspects and the practical realization within the environment of the commercial Finite Element and the Multi Body Systems software packages, ANSYS and SIMPACK respectively. In this regard, a variety of structure preserving Model Order Reduction methods is presented and a categorization methodology is provided in view of the later FEM-MBS coupling process. The algorithmic scheme of several of the MOR methods indicates the capability of generating qualitatively better Reduced Order Models than the standardized Guyan and Component Mode Synthesis approaches. The efficiency of a MOR method is measured in terms of both the quality of the ROM and the associated time required for the .computation Based on the application of the, so called, Model Correlation Criteria the efficiency of the MOR schemes is tested on four application examples originating from the area of structural mechanics, i.e. the 3D elastic solid bar structure, the UIC60 elastic rail, the elastic piston rod, and the elastic crankshaft model. Herewith, the superiority of alternative MOR schemes in comparison to Guyan or CMS methods is demonstrated in terms of the ROM?s quality and the computation time by the use of either the one-step or the two-step MOR algorithms. Numerous of the FE discretized structures suffer from the, so called, ill-conditioned properties regarding the associated stiffness matrix. On one hand, the direct solution of a MOR method might produce erroneous ROMs due to the associated truncation phenomenon and on the other hand, any kind of iterative approach suffers from vast computation times. The application of the diagonal perturbation methodology improves the condition properties of the model?s stiffness matrix and thus, both kinds of the aforementioned solution procedures are affected. The back-projection approach is introduced, which projects the ROM belonging to the Non physical subspace reduction-expansion methods category back onto the physical configuration space and thus, enabling its further usage in a MBS code, e.g. SIMPACK. Finally, the theoretical, modelling, and numerical advancements are combined in terms of the Model Order Reduction Package. The Matlab-based MORPACK toolbox enables the FEM-MBS coupling process for the ANSYS-SIMPACK utilization and herewith, several of the aforementioned enhancements are included. With the help of the two integrated inner interfaces, i.e. MOR and SID, as well as four application levels, the import into SIMPACK of alternatively free or fixed ROMs is enabled. The functionality of MORPACK is demonstrated based on two application examples, namely, the 3D elastic solid bar and the UIC60 elastic rail, the dynamic properties of which are validated prior to their import into SIMPACK.

La conception d'algorithmes pour les systèmes concurrents et répartis est subtile et difficile. Ces systèmes sont enclins à des blocages et à des conditions de course et sont par conséquent difficiles à reproduire La vérification formelle est une technique essentielle pour modéliser le système et ses propriétés et s'assurer de sa correction au moyen du model checking. Des langages formels tels TLA+ permettent de décrire des algorithmes compliqués de manière assez concise, mais les concepteurs d'algorithmes trouvent souvent difficile de modéliser un algorithme par un ensemble de formules. Dans ce mémoire nous présentons le langage PlusCal-2 qui vise à allier la simplicité de pseudo-code à la capacité d'être vérifié formellement. PlusCal-2 améliore le langage algorithmique PlusCal conçu par Lamport en levant certaines restrictions de ce langage et en y ajoutant de nouvelles constructions. Notre langage est destiné à la description d'algorithmes à un niveau élevé d'abstraction. Sa syntaxe ressemble à du pseudo-code mais il est tout à fait expressif et doté d'une sémantique formelle. Pour calculer la dépendance conditionnelle pour les algorithmes en PlusCal-2 nous exploitons des informations sur la localité des actions et nous générons des prédicats d'indépendance. Nous proposons également une adaptation d'un algorithme de réduction par ordre partiel dynamique pour une variante du model checker TLC. Enfin, nous proposons une variante d'un algorithme de réduction par ordre partiel statique s'appuyant sur une relation de dépendance constante, et son implantation au sein de TLC. Nous présentons nos résultats expérimentaux et une preuve de correction / Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, and are therefore hard to reproduce. Formal verification is a key technique to model the system and its properties and then perform verification by means of model checking. Formal languages like TLA+ have the ability to describe complicated algorithms quite concisely, but algorithm designers often find it difficult to model an algorithm in the form of formulas. In this thesis, we present PlusCal-2 that aims at being similar to pseudo-code while being formally verifiable. PlusCal-2 improves upon Lamport?s PlusCal algorithm language by lifting some of its restrictions and adding new constructs. Our language is intended for describing algorithms at a high level of abstraction. Finite instances of algorithms described in PlusCal-2 can be verified through the TLC model checker. The second contribution presented in this thesis is a study of partial-order reduction methods using conditional and constant dependency relation. To compute conditional dependency for PlusCal-2 algorithms, we exploit their locality information and present them in the form of independence predicates. We also propose an adaptation of a dynamic partial-order reduction algorithm for a variant of the tlc model checker. As an alternative to partial order reduction based on conditional dependency, we also describe a variant of a static partial-order reduction algorithm for the tlc model checker that relies on constant dependency relation. We also present our results for the experiments along with the proof of correctness