<p>In a distributed database system, pessimistic concurrency control is often used to ensure consistency which implies that the execution time of a transaction is not predictable. The execution time of a transaction is not dependent on the local transactions only, but on every transaction in the system.</p><p>In real-time database systems it is important that transactions are predictable. One way to make transactions predictable is to use eventual consistency where transactions commit locally before they are propagated to other nodes in the system. It is then possible to get predictable transactions due to the fact that the execution time of the transaction only depends on concurrent transactions on the local node and not on delays on other nodes and delays from a network.</p><p>In this report an investigation is made on how a replication protocol using eventual consistency can be designed for, and implemented in, DeeDS, a distributed real-time database prototype. The protocol consists of three parts: a propagation method, a conflict detection algorithm, and a conflict resolution mechanism. The conflict detection algorithm is based on version vectors. The focus is on the propagation mechanism and the conflict detection algorithm of the replication protocol.</p><p>An implementation design of the replication protocol is made. A discussion on how the version vectors may be applied in terms of granularity (container, page, object or attribute) and how the log filter should be designed and implemented to suit the particular conflict detection algorithm is carried out. A number of test cases with focus on regression testing have been defined.</p><p>It is concluded that the feasibility of the conflict detection algorithm is dependent on the application type that uses DeeDS.</p>

<p>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.</p><p>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.</p>

<p>To gain confidence in that a dynamic real-time system behaves correctly, we test it. Automated verification & validation can be used to conduct testing of such systems in an effective and economic way.</p><p>An event monitor can be used as a part of a test oracle to monitor the system that is being tested. The test oracle could use the data (i.e., the streams of events) derived from the tested system, to determine if an executed test case gave a positive or negative result. To do this, the test oracle compares the streams of events received from the event monitor with the event expressions derived from the formal specification, and decides if the executed test case has responded positive or negative. Any deviations between observed behaviour and accepted behaviour should be reported by the test oracle as a negative result. If the executed test case gave a negative result, the monitor part should signal this to the reporter part of the test oracle.</p><p>This work aims to investigate how the event expressions can be derived from the formal specification, and in particular, how the event specification language Solicitor can be used to represent these event expressions.</p><p>We also discuss the need for parameterized event types in Solicitor, and any other event specification languages used in event monitoring. We also show that support for parameterized event types is a significant requirement for such languages.</p>

- / -

Timed automata are a formalism to model, verify, and synthesize real-time systems. They have the advantage of having an abstract mathematical semantics, which allow formalizing and solving several verification and synthesis problems. However, timed automata are intended to design models, rather than completely describe real systems. Therefore, once the design phase is over, it remains to check whether the behavior of an actual implementation corresponds to that of the timed automaton model. An important step before implementing a system design is ensuring its robustness. This thesis considers a notion of robustness that asks whether the behavior of a given timed automaton is preserved, or can be made so, when it is subject to small perturbations. Several approaches are considered: Robustness analysis seeks to decide whether a given timed automaton tolerates perturbations, and in that case to compute the (maximum) amount of tolerated perturbations. In robust synthesis, a given system needs to be controlled by a law (or strategy) which tolerates perturbations upto some computable amount. In robust implementation, one seeks to automatically transform a given timed automaton model so that it tolerates perturbations by construction. Several perturbation models are considered, ranging from introducing error in time measures (guard enlargement), forbidding behaviors that are too close to boundaries (guard shrinking), and restricting the time domain to a discrete sampling. We also formalize robust synthesis problems as games, where the control law plays against the environment which can systematically perturb the chosen moves, by some bounded amount. These problems are studied on timed automata and their variants, namely, timed games, and weighted timed automata and games. Algorithms for the parameterized robustness analysis against guard enlargements, and guard shrinkings are presented. The robust synthesis problem is studied for two variants of the game semantics, for timed automata, games, and their weighted extensions. A software tool for robustness analysis against guard shrinkings is presented, and experimental results are discussed. The robust implementation problem is also studied in two different settings. In all algorithms, an upper bound on perturbations that the given timed automaton tolerates can be computed.

Complexity and variety of systems that are working in real time mode need to be specified regarding all behavior conditions. The correctness of the specification, determines whether implemented system will supply conditions that were set. To ensure that specification of the described real-time system is correct, we have to do verification and validation of the specification. Traditional verification methods do not assure full real time system inspection. The main drawback, talking about them, is impossibility of system evaluation according time. In this paper a reachable states graph and its generating algorithms are described, while two time moments are compared using linear programming, Simplex method. Therefore, method for checking equivalent state in system behavioral pathway was suggested. Also, theoretical reasoning for creating computer applications, which automates generation of reachable states graph, is given. Reachable states graph fully evaluates real time system behavior.

The aim of this research is to create the modeling and simulation tool for the real time systems. The component based object oriented model of real time system is introduced as solution. This model uses JAVA and XML languages to specify one component of the real time system. The model can be used to generate source code directly from components specifications. The modeling and simulation system was created based on component model. It can be used for modeling real time systems of any domain, any abstraction level or any complexity level. The experiments show that proposed modeling technique is correct.

A real-time system is one in which the correctness of the computations not only depends upon the logical correctness of the computation but also upon the time at which the result is produced. If the timing constraints of the system are not met, system failure is said to have occurred. Real-time system consist specialized hardware an software components. Nowadays, systems are so big and complex that teams of architects, analysts, programmers, testers and users must work together to create reliable real-time system. To manage this, a number of system development life cycle models have been created. System development life cycle refers to a methodology for developing systems. It provides a consistent framework of tasks and deliverables needed to develop systems. System development consist stages, that are common for all models: project planning, requirements definition, system design, implementation, testing, deployment and maintenance. However, there still are problems, that lead project to the failure. Problems appear while iterating from design stage to the implementation or prototype creation. Thesis describes methodology, that provide a way to overcome these problems. The main idea is to transform functional structure of the real-time system, that is designed using easy to understand graphical environment, to the executable code that will be able to run on target hardware components. Thesis describe the methods of doing such transformation. Methodology allows to create... [to full text]

Today's embedded distributed real-time systems, are exposed to large variations in resource usage due to complex software applications, sophisticated hardware platforms, and the impact of their run-time environment. As eciency becomes more important, the applications running on these systems are extended with on-line resource managers whose job is to adapt the system in the face of such variations. Distributed systems are often heterogeneous, meaning that the hardware platform consists of computing nodes with dierent performance, operating systems, and scheduling policies, linked through one or more networks using dierent protocols. In this thesis we explore whether resource managers used in such distributed embedded systems are stable, meaning that the system's resource usage is controlled under all possible run-time scenarios. Stability implies a bounded worst-case behavior of the system and can be linked with classic real-time systems' properties such as bounded response times for the software applications. In the case of distributed systems, the stability problem is particularly hard because software applications distributed over the dierent resources generate complex, cyclic dependencies between the resources, that need to be taken into account. In this thesis we develop a detailed mathematical model of an adaptive, distributed real-time system and we derive conditions that, if satised, guarantee its stability.

Gausybė sudėtingų realaus laiko sistemų turi būti specifikuotos įvertinant visas galimas situacijas. Specifikacijos teisingumas reiškia, kad sistema užduotomis sąlygomis pasieks norimą rezultatą. Norėdami užtikrinti, kad aprašyta specifikacija yra teisinga, reikia atlikti sistemos verifikavimą ir validavimą. Tradiciniai verifikavimo metodai neužtikrina pilno sistemos patikrinimo. Pagrindinis jų trūkumas yra tai, kad jos negali įvertinti laikinių charakteristikų. Per keletą paskutinių metų, buvo sukurti nauji metodai, kuriuose įvykių įvykimo laikas priklauso intervalams. Šiame darbe šie metodai buvo patobulinti, kad pilnai aprašytų realaus laiko sistemų veiksenas. Šiame darbe pateikiamas pasiekiamų būsenų medžio sudarymo algoritmas, kai sistemos pabaigos laikų momentų aibė priklauso bet kokiam intervalui - griežtam, negriežtam, griežtam iš kairės arba dešinės. / Complexity and variety of systems that are working in real time mode need to be specified regarding all behavior conditions. The correctness of the specification, determines whether implemented system will supply conditions that were set. To ensure that specification of the described real-time system is correct, we have to do verification and validation of the specification. Traditional verification methods do not assure full real time system inspection. The main drawback, talking about them, is impossibility of system evaluation according time. In past few years, new methods were implemented, whereat real time system events befall in time interval. In this paper, these methods were improved to fully specify real time systems behaviour. Reachable states graph and its generating algorithms are described here, wherein real time system events befall in any type of time interval – inclusive, exclusive in left, right or both sides.