| 1. |
- Lindström, Birgitta, 1958-
(författare)
-
Testability of Dynamic Real-Time Systems
- 2009
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- This dissertation concerns testability of event-triggered real-time systems. Real-time systems are known to be hard to test because they are required to function correct both with respect to what the system does and when it does it. An event-triggered real-time system is directly controlled by the events that occur in the environment, as opposed to a time-triggered system, which behavior with respect to when the system does something is constrained, and therefore more predictable. The focus in this dissertation is the behavior in the time domain and it is shown how testability is affected by some factors when the system is tested for timeliness.This dissertation presents a survey of research that focuses on software testability and testability of real-time systems. The survey motivates both the view of testability taken in this dissertation and the metric that is chosen to measure testability in an experiment. We define a method to generate sets of traces from a model by using a meta algorithm on top of a model checker. Defining such a method is a necessary step to perform the experiment. However, the trace sets generated by this method can also be used by test strategies that are based on orderings, for example execution orders.An experimental study is presented in detail. The experiment investigates how testability of an event-triggered real-time system is affected by some constraining properties of the execution environment. The experiment investigates the effect on testability from three different constraints regarding preemptions, observations and process instances. All of these constraints were claimed in previous work to be significant factors for the level of testability. Our results support the claim for the first two of the constraints while the third constraint shows no impact on the level of testability.Finally, this dissertation discusses the effect on the event-triggered semantics when the constraints are applied on the execution environment. The result from this discussion is that the first two constraints do not change the semantics while the third one does. This result indicates that a constraint on the number of process instances might be less useful for some event-triggered real-time systems.
|
|
| 2. |
- Mathiason, Gunnar, 1966-
(författare)
-
Virtual Full Replication for Scalable Distributed Real-Time Databases
- 2009
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- A fully replicated distributed real-time database provides high availability and predictable access times, independent of user location, since all the data is available at each node. However, full replication requires that all updates are replicated to every node, resulting in exponential growth of bandwidth and processing demands with the number of nodes and objects added. To eliminate this scalability problem, while retaining the advantages of full replication, this thesis explores Virtual Full Replication (ViFuR); a technique that gives database users a perception of using a fully replicated database while only replicating a subset of the data.We use ViFuR in a distributed main memory real-time database where timely transaction execution is required. ViFuR enables scalability by replicating only data used at the local nodes. Also, ViFuR enables flexibility by adaptively replicating the currently used data, effectively providing logical availability of all data objects. Hence, ViFuR substantially reduces the problem of non-scalable resource usage of full replication, while allowing timely execution and access to arbitrary data objects.In the thesis we pursue ViFuR by exploring the use of database segmentation. We give a scheme (ViFuR-S) for static segmentation of the database prior to execution, where access patterns are known a priori. We also give an adaptive scheme (ViFuR-A) that changes segmentation during execution to meet the evolving needs of database users. Further, we apply an extended approach of adaptive segmentation (ViFuR-ASN) in a wireless sensor network - a typical dynamic large-scale and resource-constrained environment. We use up to several hundreds of nodes and thousands of objects per node, and apply a typical periodic transaction workload with operation modes where the used data set changes dynamically. We show that when replacing full replication with ViFuR, resource usage scales linearly with the required number of concurrent replicas, rather than exponentially with the system size.
|
|
| 3. |
- Ericsson, AnnMarie, 1972-
(författare)
-
Enabling Tool Support for Formal Analysis of ECA Rules
- 2009
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Rule-based systems implemented as event-condition-action (ECA) rules utilize a powerful and flexible paradigm when it comes to specifying systems that need to react to complex situation in their environment. Rules can be specified to react to combinations of events occurring at any time in any order. However, the behavior of a rule based system is notoriously hard to analyze due to the rules ability to interact with each other.Formal methods are not utilized in their full potential for enhancing software quality in practice. We argue that seamless support in a high-level paradigm specific tool is a viable way to provide industrial system designers with powerful verification techniques. This thesis targets the issue of formally verifying that a set of specified rules behaves as indented.The prototype tool REX (Rule and Event eXplorer) is developed as a proof of concept of the results of this thesis. Rules and events are specified in REX which is acting as a rule-based front-end to the existing timed automata CASE tool UPPAAL. The rules, events and requirements of application design are specified in REX. To support formal verification, REX automatically transforms the specified rules to timed automata, queries the requirement properties in the model-checker provided by UPPAAL and returns results to the user of REX in terms of rules and events.The results of this thesis consist of guidelines for modeling and verifying rules in a timed automata model-checker and experiences from using and building a tool implementing the proposed guidelines. Moreover, the result of an industrial case study is presented, validating the ability to model and verify a system of industrial complexity using the proposed approach.
|
|
| 4. |
- Karlsson, Alexander
(författare)
-
Evaluating credal set theory as a belief framework in high-level information fusion for automated decision-making
- 2010
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- High-level information fusion is a research field in which methods for achieving an overall understanding of the current situation in an environment of interest are studied. The ultimate goal of these methods is to provide effective decision-support for human or automated decision-making. One of the main proposed ways of achieving this is to reduce the uncertainty, coupled with the decision, by utilizing multiple sources of information. Handling uncertainty in high-level information fusion is performed through a belief framework, and one of the most commonly used such frameworks is based on Bayesian theory. However, Bayesian theory has often been criticized for utilizing a representation of belief and evidence that does not sufficiently express some types of uncertainty. For this reason, a generalization of Bayesian theory has been proposed, denoted as credal set theory, which allows one to represent belief and evidence imprecisely. In this thesis, we explore whether credal set theory yields measurable advantages, compared to Bayesian theory, when used as a belief framework in high-level information fusion for automated decision-making, i.e., when decisions are made by some pre-determined algorithm. We characterize the Bayesian and credal operators for belief updating and evidence combination and perform three experiments where the Bayesian and credal frameworks are evaluated with respect to automated decision-making. The decision performance of the frameworks are measured by enforcing a single decision, and allowing a set of decisions, based on the frameworks’ belief and evidence structures. We construct anomaly detectors based on the frameworks and evaluate these detectors with respect to maritime surveillance. The main conclusion of the thesis is that although the credal framework uses considerably more expressive structures to represent belief and evidence, compared to the Bayesian framework, the performance of the credal framework can be significantly worse, on average, than that of the Bayesian framework, irrespective of the amount of imprecision.
|
|
