Software testing is an important process for ensuring the quality of the software. As the complexity of the software increases, traditional means of manual testing becomes increasingly more complex and time consuming. In most embedded systems, designing software with as few errors as possible is often critical. Resource usage is also of concern for proper behavior because of the very nature of embedded systems.  To design reliable and energy-efficient systems, methods are needed to detect hot points of consumption and correct them prior to deployment. To reduce testing effort, Model-based testing can be used which is one testing method that allows for automatic testing of model based systems. Model-based testing has not been investigated extensively for revealing resource usage anomalies in embedded systems. UPPAAL SMC is a statistical model checking tool which can be used to model the system’s resource usage. Currently UPPAAL SMC lacks the support for performing automatic test generation and test selection. In this thesis we provide this support with a framework for automatic test generation and test selection using mutation analysis, a method for minimizing the generated test suite while maximizing the fault coverage and a tool implementing the framework on top of the UPPAAL SMC tool. The thesis also evaluates the framework on a Brake by Wire industrial system. Our results show that we could for a Brake-by-wire system, simulated on a consumer processor with five mutants, in best case find a test case that achieved 100% mutation score within one minute and confidently identify at least one test case that achieved full mutation score within five minutes. The evaluation shows that this framework is applicable and relatively efficient on an industrial system for reducing continues resource usage target testing effort.

Embedded systems are used in many technical products of today. The tendency also points to the fact that they are in many ways becoming more and more complex as technology advances. Systems like advanced avionics, air bags, ABS brakes or any real-time embedded system requires reliability, correctness and timeliness. This puts hard pressure on designers, analyzers and developers. The need for high performance and non failing systems has therefore led to a growing interest in modeling and verification of component-based embedded systems in order to reduce costs and simplify design and development. The solution proposed by the Embedded Systems Lab at Linköping University is the modeling language PRES+, Petri Net based Representation for Embedded Systems. PRES+ models are then translated into timed automata, TA, which is used by the UPPAAL verification tool. To be able to verify timing properties the translated TA model must be instrumented with certain timers, called clocks. These clocks must be reset in a manner reflected by the property to be verified. This thesis will provide a solution to the problem and also give the reader necessary information in order to understand the theoretical background needed. The thesis will also show the reader the importance of modeling and time verification in the development of embedded systems. A simple example is used to describe and visualize the benefit regarding real-time embedded systems as well as the importance of the ability to verify these systems. The conclusion drawn stresses the fact that high development costs, possible gain of human lives and the problems in developing complex systems only emphasize the need for easy to handle and intuitive verification methods.

Event-triggered real-time systems are desirable to use in environments where the arrival of events are hard to predict. The semantics of an event-triggered system is well mapped to the behaviour of an active database management system (ADBMS), specified using event-condition-action (ECA) rules. The benefits of using an active database, such as persistent data storage, concurrency control, timely response to event occurrences etc. highlights the need for a development method for event-triggered real-time systems using active databases. However, there are problems left to be solved before an ADBMS can be used with confidence in real-time environments. The behaviour of a real-time system must be predictable, which implies a thorough analysed specification with e.g. specified worst case execution times. The predictability requirement is an obstacle for specifying real-time systems as ECA rules, since the rules may affect each other in many intricate ways which makes them hard to analyse. The interaction between the rules implies that it is not enough to verify the correctness of single rules; an analysis must consider the behaviour of the entire rule set. In this dissertation, an approach for developing active applications is presented. A method is examined which starts with an analysed high-level timed automaton specification and transforms the specified behaviour into an implicitly analysed rule set. For this method to be useful, the transformation from timed automata to rules must preserve the exact behaviour of the high level specification. Hence, the aim of this dissertation is to verify transformations between timed automaton specifications and ECA rules. The contribution of this project is a structured set of general transformations between timed automata specifications and ECA rules. The transformations include both transformations of small timed automata constructs for deterministic environments and formally verified timed automata patterns specifying the behaviour of composite events in recent and chronicle context.

Real-time systems are required to answer to external stimuli within a specified time-period. For this to be possible, the systems behaviour must be predictable. The use of active databases in real-time systems introduces unpredictability in the system, e.g. due to their use of active rules. The behaviour in active databases is usually specified in ECA-rules. Sets of ECA-rules are hard to analyse, which implies that the behaviour of the ECA-rule set is hard to predict. The purpose of this project is to evaluate the ability to support the development of a predictable ECA-rule set. Using a formal method for the specification task is desirable, since a formal specification is analysable and can be proven correct. In this project, timed-automata are used for specifying the systems behaviour. A method for deriving predictable ECA-rules from a timed-automaton specification is developed, and successfully applied on a case-study specification. For this case-study specification, a set of ECA-rules preserving the analysed behaviour of the timed-automata specification is derived.

Random number generators are basic building blocks of modern cryptographic systems. Usually pseudo random number generators, carefully constructed deter- ministic algorithms that generate seemingly random numbers, are used. These are built upon foundations of thorough mathematical analysis and have been subjected to stringent testing to make sure that they can produce pseudo random sequences at a high bit-rate with good statistical properties. A pseudo random number generator must be initiated with a starting value. Since they are deterministic, the same starting value used twice on the same pseudo random number generator will produce the same seemingly random sequence. Therefore it is of utmost importance that the starting value contains enough en- tropy so that the output cannot be predicted or reproduced in an attack. To gen- erate a high entropy starting value, a true random number generator that uses sampling of some physical non-deterministic phenomenon to generate entropy, can be used. These are generally slower than their pseudo random counterparts but in turn need not generate the same amount of random values. In field programmable gate arrays (FPGA), generating random numbers is not trivial since they are built upon digital logic. A popular technique to generate entropy within a FPGA is to sample jittery clock signals. A quite recent technique proposed to create a robust clock signals, that contains such jitter, is to use self- timed ring oscillators. These are structures in which several events can propagate freely at an evenly spaced phase distribution. In this thesis self-timed rings of six different lengths is implemented on a spe- cific FPGA hardware. The different implementations are tested with the TestU01 test suite. The results show that two of the implementations have a good oscilla- tory behaviour that is well suited for use as random number generators. Others exhibit unexpected behaviours that are not suited to be used in a random num- ber generator. Two of the implemented random generators passed all tests in the TestU01 batteries Alphabit and BlockAlphabit. One of the generators was deemed not fit for use in a random number generator after failing all of the tests. The last three were not subjected to any tests since they did not behave as ex- pected.

No description available.

We present a pattern system for property specification. It extends the existing patterns identified in [4] which allow to reason about occurrence and order of events, but not about time conditions. Introducing time-related patterns allows the specification of real-time requirements. The paper is limited to 3 pages. Therefore it contains only basic ideas. The details can be found in [9].

This project was undertaken to establish whether the Onderstepoort Biological Products Fowl Typhoid (OBPft) vaccine registered as an injectable vaccine was effective and safe when administered orally to commercial layers. Its efficacy and duration of protection were compared to the intramuscular injectable route. Commercial brown layer hens were used as they were found to be highly susceptible to Salmonella gallinarum infections. In the safety trial birds were euthanased at timed intervals spanning 4-weeks post vaccination. Necropsies were performed and samples were taken and tested. No clinical signs or mortalities could be attributed to the OBPft vaccine. No active shedding of the vaccine strain could be detected. Slight pathological changes were noted with both routes of vaccination; however these changes were transient, returning to normal within the observation period. The injected group showed a better serological response with the serum agglutination test than the orally vaccinated groups. In the duration of protection trial the two routes of vaccination were compared, the birds were challenged at three 8-week intervals post vaccination. All the unvaccinated birds died. The protection offered to the vaccinated groups was good when birds were challenged 8 and 16-weeks after vaccination. However, this dipped steeply by the challenge 24-weeks post vaccination. Statistically (ANOVA, p<0.05) it was found that there was no significant difference between the protection offered by either the oral or injected route of vaccination with the OBPft vaccine. / Dissertation (MSc (Veterinary Science))--University of Pretoria, 2006. / Production Animal Studies / unrestricted

No description available.

The present study involves the creation and analysis of a corpus containing 7747 samples of timed, pre-matriculated L2 English writing from an IEP. The focus of the analysis is on three phrasal complexity measures with time and proficiency as fixed effects, examining their impact on each measure. Results of the analysis suggest that this is true for some phrasal measures, such as nominalizations and attributive adjectives, while others, such as noun-noun phrases, may indicate a lower level of proficiency or lesser allotted writing time. Nominalizations in particular demonstrated a strong relationship with both allotted time and proficiency, further suggesting that certain phrasal measures may be more useful than others when examining academic writing, and therefore may merit additional focus and time spent on related structures in IEPs and other pre-matriculated ESL/EFL classrooms.