This dissertation shows that the bounded property verification of hardware Register Transfer Level (RTL) designs can be efficiently performed by precise abstract interpretation of a software representation of the RTL. The first part of this dissertation presents a novel framework for RTL verification using native software analyzers. To this end, we first present a translation of the hardware circuit expressed in Verilog RTL into the software in C called the software netlist. We then present the application of native software analyzers based on SAT/SMT-based decision procedures as well as abstraction-based techniques such as abstract interpretation for the formal verification of the software netlist design generated from the hardware RTL. In particular, we show that the path-based symbolic execution techniques, commonly used for automatic test case generation in system softwares, are also effective for proving bounded safety as well as detecting bugs in the software netlist designs. Furthermore, by means of experiments, we show that abstract interpretation techniques, commonly used for static program analysis, can also be used for bounded as well as unbounded safety property verification of the software netlist designs. However, the analysis using abstract interpretation shows high degree of imprecision on our benchmarks which is handled by manually guiding the analysis with various trace partitioning directives. The second part of this dissertation presents a new theoretical framework and a practical instantiation for automatically refining the precision of abstract interpretation using Conflict Driven Clause Learning (CDCL)-style analysis. The theoretical contribution is the abstract interpretation framework that generalizes CDCL to precise safety verification for automatic transformer refinement called Abstract Conflict Driven Learning for Safety (ACDLS). The practical contribution instantiates ACDLS over a template polyhedra abstract domain for bounded safety verification of the software netlist designs. We experimentally show that ACDLS is more efficient than a SAT-based analysis as well as sufficiently more precise than a commercial abstract interpreter.

L'Ingénierie des Systèmes (IS) est une approche pluridisciplinaire et collaborative pour mener à bâtir et structurer la conception puis la réalisation et le développement de systèmes complexes. L’IS repose à la fois sur une approche processus et sur la mise en oeuvre de modèles de systèmes s'appuyant de fait dans un contexte basé ou dirigé par des modèles. On parle alors d’Ingénierie Système Basée sur des Modèles (ISBM ou Model based Systems Engineering MBSE). L’ISBM introduit des concepts, méthodes et techniques pour construire et gérer des modèles. Elle a pour objectif l’atteinte et l’amélioration de leur qualité afin de procurer aux parties prenantes un degré de confiance jugé suffisant pour aider la prise des décisions de conception, d'amélioration et de réalisation. Ces décisions conditionnent le fonctionnement, la sûreté, la sécurité, les coûts, et plus généralement tout un ensemble de propriétés attendues à la fois du modèle comme du système modélisé, tout au long de la phase aval de l’ingénierie et de développement, jusqu’à la réalisation et au déploiement du système. La qualité des modèles est obtenue au travers des processus de Vérification et Validation (V&V). Les objectifs sont alors d’assurer que les modèles soient cohérents, bien formés, bien construits et représentés correctement. En effet, aux yeux des parties prenantes, les modèles doivent être fiables, fidèles et pertinents au regard des besoins des concepteurs, représentant aussi précisément que possible le point de vue du système en cours de conception. Des langages de modélisation dit « métier » (Domain Specific Modelling Languages ou DSML) sont spécifiquement créés pour pouvoir fournir des représentations i.e. des modèles dans les différents points de vue sur le système. Un DSML est basé sur une syntaxe et sur une sémantique. La sémantique de ces langages est en général fournie par des approches externes (vérificateurs de modèles). Ces dernières sont, à notre sens, une limitation clé pour le déploiement des stratégies de V&V dans le contexte de l’ISBM. En réponse à cette limitation, la contribution conceptuelle de cette thèse est présentée sous la forme d’un nouveau langage de métamodélisation, nommé xviCore (noyau exécutable, vérifiable et interopérable). xviCore fournit les concepts et les principes pour définir puis vérifier et valdier la syntaxe et la sémantique en phase de construction de tels DSML en combinant trois métalangages : un métalangage orienté objet pour la conception de la partie syntaxique, un métalangage pour la conception du comportement et un métalangage pour la conception de propriétés formelles. La contribution méthodologique de ces travaux permet ensuite le déploiement d’une stratégie de V&V «directe» en lieu et place des traditionnelles approches externes. Elle est basée sur la simulation et la preuve formelle de propriétés. Le mécanisme de simulation permet d’observer le comportement des modèles de systèmes au travers de leur exécution, tandis que le mécanisme de preuve permet de spécifier et ensuite de vérifier des propriétés formelles. La contribution technique se compose d’un ensemble des plugins Eclipse qui implémentent le métalangage xviCore, le mécanisme de simulation et le mécanisme de la preuve formelle. / Systems Engineering (SE) is an interdisciplinary and collaborative approach for successful design and management of large scale complex systems. Among other principles, SE promotes and mandates a model-based (or model-driven) approach for all stages of system design processes, denoted Model-Based Systems Engineering (MBSE). This implies concepts, techniques and tools for creating and managing various systems models for the purpose of stakeholders, and for reaching and improving the quality of models helping then stakeholders during decision-making processes, to make decisions faster and efficiently with enough confidence. Indeed, these decisions impact all along the downstream phases of system engineering and development until the realization and deployment of the real system, its functioning, safety, security, induced costs and so on. In this work, a particular attention is given to model verification and validation (V&V). The goals are to assure prior to decision-making processes, first, that models are coherent, well-formed and correctly build and represented, and second, that they are trustworthy and relevant, representing as accurately as possible the viewpoints of a system under design as expected by stakeholders.Such models provide stakeholders with confidence and trust, aiding them in making, but also in arguing decisions. Models are created by using modeling languages that are specifically tailored for a given viewpoint of a system, denoted Domain Specific Modeling Languages (DSMLs).The basic principles on which a DSML is based are its syntax and its semantics, but current DSMLs have been more studied from the syntactical point than from the semantical one that is often neglected or, when needed, provided by means of translating the DSML into third party formalisms. This is the key limitation preventing the deployment of a successful V&V strategy in MBSE context. To overcome this shortcoming, this thesis proposes first a conceptual contribution consisting of a new metamodeling language, called eXecutable, Verifiable and Interoperable Core (xviCore), allowing stakeholders to build DSMLs (called xviDSMLs), that along with their syntax also integrates semantics. Our solution combines, three meta-languages, an object-oriented metamodeling language for the specification of the syntactical part with a formal behavioral modeling language and a property modeling language for the semantical part. The methodological contribution of this work allows the deployment of successful V&V strategies allowing for direct (without transformation) model verification by simulation and properties proof. We propose a mechanism to simulate the expected behavior of a SoI through model execution based on the blackboard-based communication model, and a mechanism for specification and verification of formal properties. The technical contribution consists of an Eclipse-EMF deployable plug-in that implements the metamodeling language xviCore and the mechanisms for simulation and formal property verification.

Examensarbetet utförs under sista årets energiingenjörsstudier vid Mälardalens högskola. Med hjälp av Ramböll Västerås utfördes en energiuppföljning av energiförbrukningen vid Hälleborgs äldreboende beläget på Bäckby i Västerås åt Västerås stad. Hälleborgs äldreboende stod klart och var fullt inflyttat våren 2015. Boendet byggdes för att möta det ökade behovet av vårdplatser i Västerås kommun. Vid byggnationen ställde kommunen ett byggkrav på 60 kWh/(m2,år) köpt energi vilket var hårdare än de gällande byggkraven som gällde i Sverige vid dåvarande tidpunkt. Under projekteringen av byggnaden ändrades kravet till 70 kWh/(m2,år) viktad energi där fjärrvärmen viktas med 1 och elen med 2.  Ändringen uppkom efter att behovet av kyla kunde lösas med ett borrhålslager vilket ger möjlighet att ta tillvara på värmen som kyls bort via värmepumpar. Byggnadens värmebehov tillgodoses av både värmepumpar och fjärrvärme vilket innebär olika energikrav enligt BBR, viktningen görs för att få ett mellanting mellan kraven för byggnad med el uppvärmning och byggnad utan eluppvärmning. Examensarbetet går ut på att utreda om byggnadens energianvändning går att följa upp efter ett år i drift. Genom att försöka beräkna förbrukningen och på den vägen upptäcka problem som behöver åtgärdas till 2 årsuppföljning 2017. Det har under arbetets gång visat sig att anläggningens mätsystem inte fungerar som tänkt vad det gäller överföring mellan fastighetens mätssystem och Västerås stads mätdata hanteringssystem Momentum. Men även när mätdatainformationen skulle hämtas manuellt visades sig att det endast fanns för ett fåtal datum vilket gjorde det omöjligt att ställa upp en årsenergi. För att kontrollera att mätningen fungerade som det skulle ställdes en sammanställning upp för perioden 2015-02-22 och 2016-03-24 vilket visade att all elproduktion inte registreras i de interna mätarna. Fjärrvärmen var enda energienhet som kunde verifieras då den förbrukningen hämtades från fjärrvärmeleverantören Mälarenergi AB. Fjärrvärmeförbrukningen uppgick till 29 kWh/ kWh/(m2,år) mot projekterade 11.7 kWh/ kWh/(m2,år). För att kunna utföra en korrekt energiuppföljning och visa tappvarmvatten förbrukningen behöver fastigheten uppdateras med fler mätare. Dels behövs en mätare som mäter levererad fjärrvärmeenergi till tappvarmvattnet och det rekommenderas även att registrera en flödesmätare på tappvarmvattnet till verksamheten. Det bör även undersökas vilka elförbrukningar som inte omfattas av internmätning för att kunna skilja verksamhets- och fastighetsenergi åt. Elenergin för undermätarna var 555 406 kWh för perioden 2015-02-22 och 2016-03-24 och motsvarnade 924 025 kWh för nätägaren Mälarenergi i perioden 2015-05-01 till 2016-04-30. För att kunna utföra en balans ska undermätarna uppgå till samma förbrukning som huvudmätaren för samma mät period. Byggnaden uppfyller idag inte förutsättningar för att kunna göra en korrekt energiuppföljning. / In order to reach the 20/20 goals (meaning 20% lower energy consumption until 2020) the energy requirements on buildings must get tougher and tougher. The city of Västerås has from year 2011 set its own energy requirements on all sold estates to 60 kWh/(m2,year). When the city needed to build the new Hälleborgs elderly care center, their aim was to reach this limited energy consumption. Soon, during the planning stage, they changed this requirement to 70 kWh/(m2,year) weighted energy. The reason for this was because they were using two heating systems, one was a electric heat pump and the second was district heating. Because of higher average age in the society, the need for more elderly care centers arise even in Västerås. In the spring 2015 Hälleborgs elderly care center was completed and occupied. 2 year after the building was complete, the contractor has to do an energy monitoring and see if the goal 70 kWh/m2 is reached. In this bachelor thesis all information will be tested and the aim is to try to make a energy monitoring and figure out what needs to be done to be able to performe the energy monitoring 2017. During the work the biggest problem has been to get the right information. The system that should keep all the measured data (Momentum) was found not to have the connection to the building. When we try to pick the data by hand from the building it was not complete. So the conclusion is that the building is not ready to energy monitoring jet. This is because the building needs more time to be stable and adjust the technical systems. It also needs more points of energy measurments and flowmeters in order to get the heating water consumption. In the electric system first the net owners energy meter is installed, then the building has own meters at each electric central to separate customers consumption from building consumption. When groups of energy is summarized, it is just half of the net owners consumption. This is because some of the energy in the building is not registered. One of the electric energy’s that not is registered is the commercial kitchen, but the difference is to big that it need to be evaluated what’s missed.