<p>Rising complexity in the development of real-time systems has made it crucial to have reusable components and a more flexible way of configuring these components into a coherent system. Aspect-oriented system development (AOSD) is a technique that allows one to put a system’s crosscutting concerns into"modules"that are called aspects. Applying AOSD in real-time and embedded system development one can expect reductions in the complexity of the system design and development. </p><p>A problem with AOSD in its current form is that it does not support predictability in the time domain. Hence, in order to use AOSD in real-time system development, we need to provide ways of analyzing temporal behavior of aspects, components and resulting system (made from weaving aspects and components). Aspect analyzer is a tool that computes the worst-case execution time (WCET) for a set of components and aspects, thus, enabling support for predictability in the time domain of aspect-oriented real-time software. </p><p>A limitation of the aspect analyzer, until now, were that no verification had been made whether the aspect analyzer would produce WCET values that were close to the measured or computed (with another WCET analysis technique) WCET of an aspect-oriented real-time system. Therefore, in this thesis we perform a verification of the correctness of the aspect analyzer using a number of different methods for WCET analysis. These investigations of the correctness of the output from the aspect analyzer gave confidence to the automated WCET analysis. In addition, performing this verification led to the identification of the steps necessary to compute the WCETs of a piece of program, when using a third party tool, which gives the ability to write accurate input files for the aspect analyzer.</p>

<p>Increasing complexity of real-time systems and demands for enabling their configurability and tailorability are strong motivations for applying new software engineering principles such as aspect-oriented and component-based software development. The integration of these two techniques into real-time systems development would enable: (i) efficient system configuration from the components in the component library based on the system requirements, (ii) easy tailoring of components and/or a system for a specific application by changing the behavior (code) of the component by aspect weaving, and (iii) enhanced flexibility of the real-time and embedded software through the notion of system configurability and component tailorability.</p><p>In this thesis we focus on applying aspect-oriented and component-based software development to real-time system development. We propose a novel concept of aspectual component-based real-time system development (ACCORD). ACCORD introduces the following into real-time system development: (i) a design method that assumes the decomposition of the real-time system into a set of components and a set of aspects, (ii) a real-time component model denoted RTCOM that supports aspect weaving while enforcing information hiding, (iii) a method and a tool for performing worst-case execution time analysis of different configurations of aspects and components, and (iv) a new approach to modelling of real-time policies as aspects.</p><p>We present a case study of the development of a configurable real-time database system, called COMET, using ACCORD principles. In the COMET example we show that applying ACCORD does have an impact on the real-time system development in providing efficient configuration of the real-time system. Thus, it could be a way for improved reusability and flexibility of real-time software, and modularization of crosscutting concerns.</p><p>In connection with development of ACCORD, we identify criteria that a design method for component-based real-time systems needs to address. The criteria include a well-defined component model for real-time systems, aspect separation, support for system configuration, and analysis of the composed real-time system. Using the identified set of criteria we provide an evaluation of ACCORD. In comparison with other approaches, ACCORD provides a distinct classification of crosscutting concerns in the real-time domain into different types of aspects, and provides a real-time component model that supports weaving of aspects into the code of a component, as well as a tool for temporal analysis of the weaved system.</p> / Report code: LiU-TEK-LIC-2003:23.

<p>Testing is the dominant verification technique used in the software industry today. The use of automatic test case execution increases, but the creation of test cases remains manual and thus error prone and expensive. To automate generation and selection of test cases, model-based testing techniques have been suggested.</p><p>In this thesis two central problems in model-based testing are addressed: the problem of how to formally specify coverage criteria, and the problem of how to generate a test suite from a formal timed system model, such that the test suite satisfies a given coverage criterion. We use model checking techniques to explore the state-space of a model until a set of traces is found that together satisfy the coverage criterion. A key observation is that a coverage criterion can be viewed as consisting of a set of items, which we call coverage items. Each coverage item can be treated as a separate reachability problem. </p><p>Based on our view of coverage items we define a language, in the form of parameterized observer automata, to formally describe coverage criteria. We show that the language is expressive enough to describe a variety of common coverage criteria described in the literature. Two algorithms for test case generation with observer automata are presented. The first algorithm returns a trace that satisfies all coverage items with a minimum cost. We use this algorithm to generate a test suite with minimal execution time. The second algorithm explores only states that may increase the already found set of coverage items. This algorithm works well together with observer automata.</p><p>The developed techniques have been implemented in the tool CoVer. The tool has been used in a case study together with Ericsson where a WAP gateway has been tested. The case study shows that the techniques have industrial strength.</p>

Our main focus in this thesis is on providing guidelines, methods, and tools for design, configuration, and analysis of configurable and reusable real-time software, developed using a combination of aspect-oriented and component-based software development. Specifically, we define a reconfigurable real-time component model (RTCOM) that describes how a real-time component, supporting aspects and enforcing information hiding, could efficiently be designed and implemented. In this context, we outline design guidelines for development of real-time systems using components and aspects, thereby facilitating static configuration of the system, which is preferred for hard real-time systems. For soft real-time systems with high availability requirements we provide a method for dynamic system reconfiguration that is especially suited for resourceconstrained real-time systems and it ensures that components and aspects can be added, removed, or exchanged in a system at run-time. Satisfaction of real-time constraints is essential in the real-time domain and, for real-time systems built of aspects and components, analysis is ensured by: (i) a method for aspectlevel worst-case execution time analysis; (ii) a method for formal verification of temporal properties of reconfigurable real-time components; and (iii) a method for maintaining quality of service, i.e., the specified level of performance, during normal system operation and after dynamic reconfiguration. We have implemented a tool set with which the designer can efficiently configure a real-time system to meet functional requirements and analyze it to ensure that non-functional requirements in terms of temporal constraints and available memory are satisfied. In this thesis we present a proof-of-concept implementation of a configurable embedded real-time database, called COMET. The implementation illustrates how our methods and tools can be applied, and demonstrates that the proposed solutions have a positive impact in facilitating efficient development of families of realtime systems.

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

Neuroprosthetics is at the intersection of neuroscience, biomedical engineering, and physics. A biocompatible neuroprosthesis contains artificial neurons exhibiting biophysically plausible dynamics. Hybrid systems analysis could be used to prototype such artificial neurons. Biohybrid systems are composed of artificial and living neurons coupled via real-time computing and dynamic clamp. Model neurons must be thoroughly tested before coupled with a living cell. We use bifurcation theory to identify hazardous regimes of activity that may compromise biocompatibility and to identify control strategies for regimes of activity desirable for functional behavior. We construct real-time artificial neurons for the analysis of hybrid systems and demonstrate a mechanism through which an artificial neuron could maintain duty cycle independent of variations in period.

In this dissertation, we implement efficient lock-based synchronization by a novel, high performance, simple and scalable hardware technique and associated software for a target shared-memory multiprocessor System-on-a-Chip (SoC). The custom hardware part of our solution is provided in the form of an intellectual property (IP) hardware unit which we call the SoC Lock Cache (SoCLC). SoCLC provides effective lock hand-off by reducing on-chip memory traffic and improving performance in terms of lock latency, lock delay and bandwidth consumption. The proposed solution is independent from the memory hierarchy, cache protocol and the processor architectures used in the SoC, which enables easily applicable implementations of the SoCLC (e.g., as a reconfigurable or partially/fully custom logic), and which distinguishes SoCLC from previous approaches. Furthermore, the SoCLC mechanism has been extended to support priority inheritance with an immediate priority ceiling protocol (IPCP) implemented in hardware, which enhances the hard real-time performance of the system. Our experimental results in a four-processor SoC indicate that SoCLC can achieve up to 37% overall speedup over spin-lock and up to 48% overall speedup over MCS for a microbenchmark with false sharing. The priority inheritance implemented as part of the SoCLC hardware, on the other hand, achieves 1.43X speedup in overall execution time of a robot application when compared to the priority inheritance implementation under the Atalanta real-time operating system. Furthermore, it has been shown that with the IPCP mechanism integrated into the SoCLC, all of the tasks of the robot application could meet their deadlines (e.g., a high priority task with 250us worst case response time could complete its execution in 93us with SoCLC, however the same task missed its deadline by completing its execution in 283us without SoCLC). Therefore, with IPCP support, our solution can provide better real-time guarantees for real-time systems. To automate SoCLC design, we have also developed an SoCLC-generator tool, PARLAK, that generates user specified configurations of a custom SoCLC. We used PARLAK to generate SoCLCs from a version for two processors with 32 lock variables occupying 2,520 gates up to a version for fourteen processors with 256 lock variables occupying 78,240 gates.

One of the key challenges in service-oriented systems engineering is the prediction and assurance of non-functional properties, such as the reliability and the availability of composite interorganizational services. Such systems are often characterized by a variety of inherent uncertainties, which must be addressed in the modeling and the analysis approach. The different relevant types of uncertainties can be categorized into (1) epistemic uncertainties due to incomplete knowledge and (2) randomization as explicitly used in protocols or as a result of physical processes. In this report, we study a probabilistic timed model which allows us to quantitatively reason about nonfunctional properties for a restricted class of service-oriented real-time systems using formal methods. To properly motivate the choice for the used approach, we devise a requirements catalogue for the modeling and the analysis of probabilistic real-time systems with uncertainties and provide evidence that the uncertainties of type (1) and (2) in the targeted systems have a major impact on the used models and require distinguished analysis approaches. The formal model we use in this report are Interval Probabilistic Timed Automata (IPTA). Based on the outlined requirements, we give evidence that this model provides both enough expressiveness for a realistic and modular specifiation of the targeted class of systems, and suitable formal methods for analyzing properties, such as safety and reliability properties in a quantitative manner. As technical means for the quantitative analysis, we build on probabilistic model checking, specifically on probabilistic time-bounded reachability analysis and computation of expected reachability rewards and costs. To carry out the quantitative analysis using probabilistic model checking, we developed an extension of the Prism tool for modeling and analyzing IPTA. Our extension of Prism introduces a means for modeling probabilistic uncertainty in the form of probability intervals, as required for IPTA. For analyzing IPTA, our Prism extension moreover adds support for probabilistic reachability checking and computation of expected rewards and costs. We discuss the performance of our extended version of Prism and compare the interval-based IPTA approach to models with fixed probabilities. / Eine der wichtigsten Herausforderungen in der Entwicklung von Service-orientierten Systemen ist die Vorhersage und die Zusicherung von nicht-funktionalen Eigenschaften, wie Ausfallsicherheit und Verfügbarkeit von zusammengesetzten, interorganisationellen Diensten. Diese Systeme sind oft charakterisiert durch eine Vielzahl von inhärenten Unsicherheiten, welche sowohl in der Modellierung als auch in der Analyse eine Rolle spielen. Die verschiedenen relevanten Arten von Unsicherheiten können eingeteilt werden in (1) epistemische Unsicherheiten aufgrund von unvollständigem Wissen und (2) Zufall als Mittel in Protokollen oder als Resultat von physikalischen Prozessen. In diesem Bericht wird ein probabilistisches, Zeit-behaftetes Modell untersucht, welches es ermöglicht quantitative Aussagen über nicht-funktionale Eigenschaften von einer eingeschränkten Klasse von Service-orientierten Echtzeitsystemen mittels formaler Methoden zu treffen. Zur Motivation und Einordnung wird ein Anforderungskatalog für probabilistische Echtzeitsysteme mit Unsicherheiten erstellt und gezeigt, dass die Unsicherheiten vom Typ (1) und (2) in den untersuchten Systemen einen Ein uss auf die Wahl der Modellierungs- und der Analysemethode haben. Als formales Modell werden Interval Probabilistic Timed Automata (IPTA) benutzt. Basierend auf den erarbeiteten Anforderungen wird gezeigt, dass dieses Modell sowohl ausreichende Ausdrucksstärke für eine realistische und modulare Spezifikation als auch geeignete formale Methoden zur Bestimmung von quantitativen Sicherheits- und Zuverlässlichkeitseigenschaften bietet. Als technisches Mittel für die quantitative Analyse wird probabilistisches Model Checking, speziell probabilistische Zeit-beschränkte Erreichbarkeitsanalyse und Bestimmung von Erwartungswerten für Kosten und Vergütungen eingesetzt. Um die quantitative Analyse mittels probabilistischem Model Checking durchzuführen, wird eine Erweiterung des Prism-Werkzeugs zur Modellierung und Analyse von IPTA eingeführt. Die präsentierte Erweiterung von Prism ermöglicht die Modellierung von probabilistischen Unsicherheiten mittelsWahrscheinlichkeitsintervallen, wie sie für IPTA benötigt werden. Zur Verifikation wird probabilistische Erreichbarkeitsanalyse und die Berechnung von Erwartungswerten durch das Werkzeug unterstützt. Es wird die Performanz der Prism-Erweiterung untersucht und der Intervall-basierte IPTA-Ansatz mit Modellen mit festen Wahrscheinlichkeitswerten verglichen.

<p>When exploring a verification approach for Komatsu Forest's control system regarding their forest machines (Valmet), the context of soft real-time systems is illuminated. Because of the nature of such context, the verification process is based on empirical corroboration of requirements fulfillment rather than being a formal proving process.</p><p>After analysis of the literature with respect to the software testing field, two paradigms have been defined in order to highlight important concepts for soft real-time systems. The paradigms are based on an abstract stimuli/response model, which conceptualize a system with inputs and output. Since the system is perceived as a black box, its internal details are hidden and thus focus is placed on a more abstract level.</p><p>The first paradigm, the “input data paradigm”, is concerned about what data to input to the system. The second paradigm, the “input data mechanism paradigm” is concerned about how the data is sent, i.e. the actual input mechanism is focused. By specifying different dimensions associated with each paradigm, it is possible to define their unique characteristics. The advantage of this kind of theoretical construction is that each paradigm creates an unique sub-field with its own problems and techniques.</p><p>The problems defined for this thesis is primarily focused on the input data mechanism paradigm, where devised dimensions are applied. New verification techniques are deduced and analyzed based on general software testing principles. Based on the constructed theory, a test system architecture for the control system is developed. Finally, an implementation is constructed based on the architecture and a practical scenario. Its automation capability is then assessed.</p><p>The practical context for the thesis is a new simulator under development. It is based upon LabVIEW and PXI technology and handles over 200 I/O. Real machine components are connected to the environment, together with artificial components that simulate the engine, hydraulic systems and a forest. Additionally, physical control sticks and buttons are connected to the simulator to enable user testing of the machine being simulated.</p><p>The results associated with the thesis is first of all that usable verification techniques were deduced. Generally speaking, some of these techniques are scalable and are possible to apply for an entire system, while other techniques may be appropriate for selected subsets that needs extra attention. Secondly, an architecture for an automated test system based on a selection of techniques has been constructed for the control system.</p><p>Last but not least, as a result of this, an implementation of a general test system has been possible and successful. The implemented test system is based on both C# and LabVIEW. What remains regarding the implementation is primarily to extend the system to include the full scope of features described in the architecture and to enable result analysis.</p> / <p>Då verifikationstekniker för Komatu Forests styrsystem utreds angående Valmet skogsmaskiner, hamnar det mjuka realtidssystemkontextet i fokus. Ett sådant kontext antyder en process där empirisk styrkning av kravuppfyllande står i centrum framför formella bevisföringsprocesser.</p><p>Efter en genomgång och analys av litteratur för mjukvarutestområdet har två paradigmer definierats med avsikten att belysa viktiga concept för mjuka realtidssystem. Paradigmerna är baserade på en abstrakt stimuli/responsmodell, som beskriver ett system med in- och utdata. Eftersom detta system betraktas som en svart låda är inre detaljer gömda, vilket medför att fokus hamnar på ett mer abstrakt plan.</p><p>Det första paradigmet benämns som “indata-paradigmet” och inriktar sig på vilket data som skickas in i systemet. Det andra paradigmet går under namnet “indatamekanism-paradigmet” och behandlar hur datat skickas in i systemet, dvs fokus placeras på själva inskickarmekanismen. Genom att definiera olika</p><p>dimensioner för de två paradigmen, är det möjligt att beskriva deras utmärkande drag. Fördelen med att använda denna teoretiska konstruktion är att ett paradigm skapar ett eget teoriområde med sina egna frågeställningar och tekniker.</p><p>De problem som definierats för detta arbete är främst fokuserade på indatamekanism-paradigmet, där framtagna dimensioner tillämpas. Nya verifikationstekniker deduceras och analyseras baserat på generella mjukvarutestprinciper. Utifrån den skapade teorin skapas en testsystemarkitektur för kontrollsystemet. Sedan utvecklas ett testsystem baserat på arkitekturen samt ett praktiskt scenario med syftet att utreda systemets automationsgrad.</p><p>Den praktiska miljön för detta arbete kretsar kring en ny simulator under utveckling. Den är baserad på LabVIEW och PXI-teknik och hanterar över 200 I/O. Verkliga maskinkomponenter ansluts till denna miljö tillsammans med konstgjorda komponenter som simulerar motorn, hydralik samt en skog. Utöver detta, ansluts styrspakar och knappar för att möjliggöra användarstyrning av maskinen som simuleras.</p><p>Resultatet förknippat med detta arbete är för det första användbara verifikationstekniker. Man kan generellt säga att några av dessa tekniker är skalbara och därmed möjliga att tillämpa för ett helt system. Andra tekniker är ej skalbara, men lämpliga att applicera på en systemdelmängd som behöver testas mer utförligt.</p><p>För det andra, en arkitektur har konstruerats för kontrollsystemet baserat på ett urval av tekniker. Sist men inte minst, som en följd av ovanstående har en lyckad implementation av ett generellt testsystem utförts. Detta system implementerades med hjälp av C# och LabVIEW. Det som återstår beträffande implementationen är att utöka systemet så att alla funktioner som arkitekturen beskriver är inkluderade samt att införa resultatanalys.</p>

This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.