Mit zunehmender Komplexität technischer Softwaresysteme ist die Nachfrage an produktiveren Methoden und Werkzeugen auch im sicherheitskritischen Umfeld gewachsen. Da insbesondere objektorientierte und modellbasierte Ansätze und Methoden ausgezeichnete Eigenschaften zur Entwicklung großer und komplexer Systeme besitzen, ist zu erwarten, dass diese in naher Zukunft selbst bis in sicherheitskritische Bereiche der Softwareentwicklung vordringen. Mit der Unified Modeling Language Real-Time (UML-RT) wird eine Softwareentwicklungsmethode für technische Systeme durch die Object Management Group (OMG) propagiert. Für den praktischen Einsatz im technischen und sicherheitskritischen Umfeld muss diese Methode nicht nur bestimmte technische Eigenschaften, beispielsweise temporale Analysierbarkeit, besitzen, sondern auch in einen bestehenden Qualitätssicherungsprozess integrierbar sein. Ein wichtiger Aspekt der Integration der UML-RT in ein qualitätsorientiertes Prozessmodell, beispielsweise in das V-Modell, ist die Verfügbarkeit von ausgereiften Konzepten und Methoden für einen systematischen Modultest. <br><br> Der Modultest dient als erste Qualititätssicherungsphase nach der Implementierung der Fehlerfindung und dem Qualitätsnachweis für jede separat prüfbare Softwarekomponente eines Systems. Während dieser Phase stellt die Durchführung von systematischen Tests die wichtigste Qualitätssicherungsmaßnahme dar. Während zum jetzigen Zeitpunkt zwar ausgereifte Methoden und Werkzeuge für die modellbasierte Softwareentwicklung zur Verfügung stehen, existieren nur wenig überzeugende Lösungen für eine systematische modellbasierte Modulprüfung. <br><br> Die durchgängige Verwendung ausführbarer Modelle und Codegenerierung stellen wesentliche Konzepte der modellbasierten Softwareentwicklung dar. Sie dienen der konstruktiven Fehlerreduktion durch Automatisierung ansonsten fehlerträchtiger, manueller Vorgänge. Im Rahmen einer modellbasierten Qualitätssicherung sollten diese Konzepte konsequenterweise in die späteren Qualitätssicherungsphasen transportiert werden. Daher ist eine wesentliche Forderung an ein Verfahren zur modellbasierten Modulprüfung ein möglichst hoher Grad an Automatisierung. <br><br> In aktuellen Entwicklungen hat sich für die Generierung von Testfällen auf Basis von Zustandsautomaten die Verwendung von Model Checking als effiziente und an die vielfältigsten Testprobleme anpassbare Methode bewährt. Der Ansatz des Model Checking stammt ursprünglich aus dem Entwurf von Kommunikationsprotokollen und wurde bereits erfolgreich auf verschiedene Probleme der Modellierung technischer Software angewendet. Insbesondere in der Gegenwart ausführbarer, automatenbasierter Modelle erscheint die Verwendung von Model Checking sinnvoll, das die Existenz einer formalen, zustandsbasierten Spezifikation voraussetzt. Ein ausführbares, zustandsbasiertes Modell erfüllt diese Anforderungen in der Regel. Aus diesen Gründen ist die Wahl eines Model Checking Ansatzes für die Generierung von Testfällen im Rahmen eines modellbasierten Modultestverfahrens eine logische Konsequenz.<br><br> Obwohl in der aktuellen Spezifikation der UML-RT keine eindeutigen Aussagen über den zur Verhaltensbeschreibung zu verwendenden Formalismus gemacht werden, ist es wahrscheinlich, dass es sich bei der UML-RT um eine zu Real-Time Object-Oriented Modeling (ROOM) kompatible Methode handelt. Alle in dieser Arbeit präsentierten Methoden und Ergebnisse sind somit auf die kommende UML-RT übertragbar und von sehr aktueller Bedeutung.<br><br> Aus den genannten Gründen verfolgt diese Arbeit das Ziel, die analytische Qualitätssicherung in der modellbasierten Softwareentwicklung mittels einer modellbasierten Methode für den Modultest zu verbessern. Zu diesem Zweck wird eine neuartige Testmethode präsentiert, die auf automatenbasierten Verhaltensmodellen und CTL Model Checking basiert. Die Testfallgenerierung kann weitgehend automatisch erfolgen, um Fehler durch menschlichen Einfluss auszuschließen. Das entwickelte Modultestverfahren ist in die technischen Konzepte Model Driven Architecture und ROOM, beziehungsweise UML-RT, sowie in die organisatorischen Konzepte eines qualitätsorientierten Prozessmodells, beispielsweise das V-Modell, integrierbar. / In consequence to the increasing complexity of technical software-systems the demand on highly productive methods and tools is increasing even in the field of safety-critical systems. In particular, object-oriented and model-based approaches to software-development provide excellent abilities to develop large and highly complex systems. Therefore, it can be expected that in the near future these methods will find application even in the safety-critical area. The Unified Modeling Language Real-Time (UML-RT) is a software-development methods for technical systems, which is propagated by the Object Management Group (OMG). For the practical application of this method in the field of technical and safety-critical systems it has to provide certain technical qualities, e.g. applicability of temporal analyses. Furthermore, it needs to be integrated into the existing quality assurance process. An important aspect of the integration of UML-RT in an quality-oriented process model, e.g. the V-Model, represents the availability of sophisticated concepts and methods for systematic unit-testing. <br><br> Unit-testing is the first quality assurance phase after implementation to reveal faults and to approve the quality of each independently testable software component. During this phase the systematic execution of test-cases is the most important quality assurance task. Despite the fact, that today many sophisticated, commercial methods and tools for model-based software-development are available, no convincing solutions exist for systematic model-based unit-testing. <br><br> The use of executable models and automatic code generation are important concepts of model-based software development, which enable the constructive reduction of faults through automation of error-prone tasks. Consequently, these concepts should be transferred into the testing phases by a model-based quality assurance approach. Therefore, a major requirement of a model-based unit-testing method is a high degree of automation. In the best case, this should result in fully automatic test-case generation. <br><br> Model checking already has been approved an efficient and flexible method for the automated generation of test-cases from specifications in the form of finite state-machines. The model checking approach has been developed for the verification of communication protocols and it was applied successfully to a wide range of problems in the field of technical software modelling. The application of model checking demands a formal, state-based representation of the system. Therefore, the use of model checking for the generation of test-cases is a beneficial approach to improve the quality in a model-based software development with executable, state-based models. <br><br> Although, in its current state the specification of UML-RT provides only little information on the semantics of the formalism that has to be used to specify a component’s behaviour, it can be assumed that it will be compatible to Real-Time Object-Oriented Modeling. Therefore, all presented methods and results in this dissertation are transferable to UML-RT.<br><br> For these reasons, this dissertations aims at the improvement of the analytical quality assurance in a model-based software development process. To achieve this goal, a new model-based approach to automated unit-testing on the basis of state-based behavioural models and CTL Model Checking is presented. The presented method for test-case generation can be automated to avoid faults due to error-prone human activities. Furthermore it can be integrated into the technical concepts of the Model Driven Architecture and ROOM, respectively UML-RT, and into a quality-oriented process model, like the V-Model.

Complex systems are designed using the model-based design paradigm in which mathematical models of systems are created and checked against specifications. Cyber-physical systems (CPS) are complex systems in which the physical environment is sensed and controlled by computational or cyber elements possibly distributed over communication networks. Various aspects of CPS design such as physical dynamics, software, control, and communication networking must interoperate correctly for correct functioning of the systems. Modeling formalisms, analysis techniques and tools for designing these different aspects have evolved independently, and remain dissimilar and disparate. There is no unifying formalism in which one can model all these aspects equally well. Therefore, model-based design of CPS must make use of a collection of models in several different formalisms and use respective analysis methods and tools together to ensure correct system design. To enable doing this in a formal manner, this thesis develops a framework for multi-model verification of cyber-physical systems based on behavioral semantics. Heterogeneity arising from the different interacting aspects of CPS design must be addressed in order to enable system-level verification. In current practice, there is no principled approach that deals with this modeling heterogeneity within a formal framework. We develop behavioral semantics to address heterogeneity in a general yet formal manner. Our framework makes no assumptions about the specifics of any particular formalism, therefore it readily supports various formalisms, techniques and tools. Models can be analyzed independently in isolation, supporting separation of concerns. Mappings across heterogeneous semantic domains enable associations between analysis results. Interdependencies across different models and specifications can be formally represented as constraints over parameters and verification can be carried out in a semantically consistent manner. Composition of analysis results is supported both hierarchically across different levels of abstraction and structurally into interacting component models at a given level of abstraction. The theoretical concepts developed in the thesis are illustrated using a case study on the hierarchical heterogeneous verification of an automotive intersection collision avoidance system.

abstract: As the complexity of robotic systems and applications grows rapidly, development of high-performance, easy to use, and fully integrated development environments for those systems is inevitable. Model-Based Design (MBD) of dynamic systems using engineering software such as Simulink® from MathWorks®, SciCos from Metalau team and SystemModeler® from Wolfram® is quite popular nowadays. They provide tools for modeling, simulation, verification and in some cases automatic code generation for desktop applications, embedded systems and robots. For real-world implementation of models on the actual hardware, those models should be converted into compilable machine code either manually or automatically. Due to the complexity of robotic systems, manual code translation from model to code is not a feasible optimal solution so we need to move towards automated code generation for such systems. MathWorks® offers code generation facilities called Coder® products for this purpose. However in order to fully exploit the power of model-based design and code generation tools for robotic applications, we need to enhance those software systems by adding and modifying toolboxes, files and other artifacts as well as developing guidelines and procedures. In this thesis, an effort has been made to propose a guideline as well as a Simulink® library, StateFlow® interface API and a C/C++ interface API to complete this toolchain for NAO humanoid robots. Thus the model of the hierarchical control architecture can be easily and properly converted to code and built for implementation. / Dissertation/Thesis / M.S. Computer Science 2013

This diploma thesis is focused on testing of Electronic Control Units, especially functional testing in which hardware and software is verified and also Model in the Loop, Software in the Loop, Processor in the Loop and Hardware in the Loop testing methods. Within practical part of this thesis testing stand for functional test of the ECU was developed and manufactured. It is connected to PC via Input/Output card, testing is controlled by MATLAB script. Whole process of testing is automated from initial upload of testing firmware to tested ECU over all phases of test up to bootloader flashing. Hardware in the Loop test was also created, in which ECU works as controller and DC motor is simulated in real time with PC in MATLAB environment.

This project has been carried out at the Electronic Embedded Systems Architecture Department at Volvo Construction Equipment (VCE), Eskilstuna, Sweden. It forms the baseline for a stepwise systematic research initiative to convert wired technologies used for certain in-vehicle control and communication components to wireless technologies. In-vehicle wireless networks are being increasingly improvised and researched to minimize the manufacturing and maintenance cost of the total amount of wiring harnesses within the vehicles. Fault tracking and maintenance becomes convenient within a wireless network. Wireless intra-vehicular communication provides an open architecture that can accommodate new components and applications. One such usability has been studied in this thesis for the Display Control Unit of Volvo paver machines. A newly designed hardware demands new technologies to ensure operator safety, security, comfort, convenience, and information. The research conducted in this thesis takes into account five probable use-cases in terms of control and communication around the new hardware, and studies suitable wireless technologies that could replace the wired technology that will be used. From a detailed literature study and the specifications provided by VCE, WAVE/IEEE802.11p and DMG/IEEE 802.11ad have been selected as optimal candidates. These two have been modelled at the physical layer of the system. After comparing the results of WAVE for 4 different channel models and 8 different coding and modulation schemes, it has been found that 1/2BPSK(3 Mbps) and 1/2 QPSK(6 Mbps) are optimal for the 3 Rician Fading Channels of Rural LOS, Urban LOS, and Highway LOS. For use-cases that involve larger distances and a large exchange of control signals, WAVE is a good choice. DMG has 19 modulation schemes for Single Carrier Modes and some of them are extremely robust at low SNR. Around SNR 20, it shows lesser packet errors than WAVE. The lower error rate is also evident from the BER values. For use-cases that involve smaller distances and a lot of image data, DMG is preferable. The work, however, does not study the safety and security aspects. Thean alysis and modelling are theoretical being based on literature studies and the necessary parameters provided by VCE. The model needs to be evaluated against field studies and practical measurements with a prototype before implementation inside the paver.

No description available.

The Hybrid Electric Vehicle Team (HEVT) of Virginia Tech is participating in the EcoCAR 3 Advanced Vehicle Technology Competition series organized by Argonne National Labs (ANL), and sponsored by General Motors (GM) and the U.S. Department of Energy (DOE). EcoCAR 3 is a 4-year collegiate competition that challenges student with redesigning a 2016 Chevrolet Camaro into a hybrid. The five main goals of EcoCAR 3 are to reduce petroleum energy use (PEU) and green house gas (GHG) emissions while maintaining safety, consumer acceptability, and performance, with an increased focus on cost and innovation. HEVT selected a P3 Plug-in Parallel hybrid electric vehicle (PHEV) to meet design goals and competition requirements. This study presents different stages of the vehicle development process (VDP) followed to integrate the HEVT Camaro. This work documents the control system development process up to Year 2 of EcoCAR 3. The modeling process to select a powertrain is the first stage in this research. Several viable powertrains and the respective vehicle technical specifications (VTS) are evaluated. The P3 parallel configuration with a V8 engine is chosen because it generated the set of VTS that best meet design goals and EcoCAR 3 requirements. The V8 engine also preserves the heritage of the Camaro, which is attractive to the established target market. In addition, E85 is chosen as the fuel for the powertrain because of the increased impact it has on GHG emissions compared to E10 and gasoline. The use of advanced methods and techniques like model based design (MBD), and rapid control prototyping (RCP) allow for faster development of engineering products in industry. Using advanced engineering techniques has a tremendous educational value, and these techniques can assist the development of a functional and safe hybrid control system. HEVT has developed models of the selected hybrid powertrain to test the control code developed in software. The strategy developed is a Fuzzy controller for torque management in charge depleting (CD) and charge sustaining (CS) modes. The developed strategy proves to be functional without having a negative impact of the energy consumption characteristics of the hybrid powertrain. Bench testing activities with the V8 engine, a low voltage (LV) motor, and high voltage (HV) battery facilitated learning about communication, safety, and functionality requirements for the three components. Finally, the process for parallel development of models and control code is presented as a way to implement more effective team dynamics. / Master of Science

With the rapid migration of physical layer design of radio towards software, it becomes necessary to select or develop the platform and tools that help in achieving rapid design and development along with flexibility and reconfigurability. The availability of field programmable gate arrays (FPGAs) has promoted the concept of reconfigurable hardware for software defined radio (SDR). It enables the designer to create high speed radios with flexibility, low latency and high throughput. Generally, the traditional method of designing FPGA based radios limits productivity. Productivity can be improved using Model based design (MBD) tools. These tools encourage a modular way of developing waveforms for radios. The tools based on MBD have been the focus of recent research exploring the concept of the platform independent model (PIM) and portability across platforms by the platform specific model (PSM). The thesis presented here explores the tools based on MBD to achieve prototyping for wireless standards like IEEE 802.11a and IEEE 802.16e on reconfigurable hardware. It also describes the interfacing of the universal software radio peripheral (USRP2), acting as a radio frequency (RF) front end, with an additional FPGA board for baseband processing. / Master of Science

For years the trend in the automotive industry has been toward more complex electronic control systems. The number of electronic control units (ECUs) in vehicles is ever increasing as is the complexity of communication networks among the ECUs. Increasing fuel economy standards and the increasing cost of fuel is driving hybridization and electrification of the automobile. Achieving superior fuel economy with a hybrid powertrain requires an effective and optimized control system. On the other hand, mathematical modeling and simulation tools have become extremely advanced and have turned simulation into a powerful design tool. The combination of increasing control system complexity and simulation technology has led to an industry wide trend toward model based control design. Rather than using models to analyze and validate real world testing data, simulation is now the primary tool used in the design process long before real world testing is possible. Modeling is used in every step from architecture selection to control system validation before on-road testing begins. The Hybrid Electric Vehicle Team (HEVT) of Virginia Tech is participating in the 2011-2014 EcoCAR 2 competition in which the team is tasked with re-engineering the powertrain of a GM donated vehicle. The primary goals of the competition are to reduce well to wheels (WTW) petroleum energy use (PEU) and reduce WTW greenhouse gas (GHG) and criteria emissions while maintaining performance, safety, and consumer acceptability. This paper will present systematic methodology for using model based design techniques for architecture selection, control system design, control strategy optimization, and controller validation to meet the goals of the competition. Simple energy management and efficiency analysis will form the primary basis of architecture selection. Using a novel method, a series-parallel powertrain architecture is selected. The control system architecture and requirements is defined using a systematic approach based around the interactions between control units. Vehicle communication networks are designed to facilitate efficient data flow. Software-in-the-loop (SIL) simulation with Mathworks Simulink is used to refine a control strategy to maximize fuel economy. Finally hardware-in-the-loop (HIL) testing on a dSPACE HIL simulator is demonstrated for performance improvements, as well as for safety critical controller validation. The end product of this design study is a control system that has reached a high level of parameter optimization and validation ready for on-road testing in a vehicle. / Master of Science

<p dir="ltr">Recent advancements in Machine Learning (ML) algorithms and increasing computational power have driven significant progress in Artificial Intelligence (AI) systems, especially those that leverage ML techniques. These AI-enabled systems incorporate components and data designed to simulate learning and problem-solving, distinguishing them from traditional systems. Despite their widespread application across various industries, certifying AI systems through verification and validation remains a formidable challenge. This difficulty primarily arises from the probabilistic nature of AI and ML components, which leads to unpredictable behaviors.</p><p dir="ltr">This dissertation investigates the verification and validation aspects within the Systems Engineering (SE) lifecycle, utilizing established frameworks and methodologies that support system realization from inception to retirement. It is comprised of three studies focused on applying formal methods, particularly model checking, to enhance the accuracy, value, and trustworthiness of models of engineered systems that use digital twins for modeling the system. The research analyzes digital twin data to understand physical asset behavior more thoroughly by applying both an exploratory method, system identification, and a confirmatory technique, machine learning. This dual approach not only aids in uncovering unknown system dynamics but also enhances the validation process, contributing to a more robust modeling framework.</p><p dir="ltr">The findings provide significant insights into the model-based design of AI-enabled digital twins, equipping systems engineers<del>,</del> and researchers with methods for effectively designing, simulating and modeling complex systems. Ultimately, this work aims to bridge the certification gap in AI-enabled technologies, thereby increasing public trust and facilitating the broader adoption of these innovative systems.</p>