157 research outputs found
On the Construction of Monitors for Temporal Logic Properties
Get PDFAbstractTemporal logic is a valuable tool for specifying correctness properties of reactive programs. With the advent of temporal logic model checkers, it has become an important aid for the verification of concurrent and reactive systems. In model checking the temporal logic properties are verified against models expressed in the tool's modelling language. In addition, model-checking techniques are useful to test actual implementations or to verify models of the system that are too detailed to be analysed by a model checker, by means of, for instance, simulation.A tableau construction is an algorithm that translates a temporal logic formula into a finite-state automaton that accepts precisely all the models of the formula. It is a key ingredient to checking satisfiability of a formula as well as to the automata-theoretic approach to model checking. An improvement to the efficiency of tableau constructions has been the development of on-the-fly versions.In this paper, we present a particular tableau construction for the incremental analysis of execution traces during test, simulation or model-checking. The automaton forms the basis of a monitor that detects both good and bad prefix of a particular kind, namely those that are informative for the property under investigation. We elaborate on the construction of the monitor and demonstrate its correctness
Synchronous dataflow scenarios
Get PDFThe Synchronous Dataflow (SDF) model of computation by Lee and Messerschmitt has become popular for modeling concurrent applications on a multiprocessor platform. It is used to obtain a guaranteed, predictable performance. The model, on the other hand, is quite restrictive in its expressivity, making it less applicable to many modern, more dynamic applications. A common technique to deal with dynamic behavior is to consider different scenarios in separation. This analysis is, however, currently limited mainly to sequential applications.
In this article, we present a new analysis approach that allows analysis of synchronous dataflow models across different scenarios of operation. The dataflow graphs corresponding to the different scenarios can be completely different. Execution times, consumption and production rates and the structure of the SDF may change. Our technique allows to derive or prove worst-case performance guarantees of the resulting model and as such extends the model-driven approach to designing predictable systems to significantly more dynamic applications and platforms. The approach is illustrated with three MP3 and MPEG-4 related case studies
QoS-Based Resource Management for Ambient Intelligence
No full textFuture homes will probably be equipped with in-home networks, combining a backbone of wired networks and a large number of devices connected through wireless links, to provide a responsive and supportive environment, known as Ambient Intelligence. Many of the applications provided to the user lean heavily on media processing and streaming data. Therefore it is expected that consumer terminals will play an important role in providing new experiences to the users. Most of the devices have to be very cost and power effective, while digital media processing is able to consume all the resources a device can offer, and more. Typically, the number of applications and the resource needs of the applications change over time. To adapt to these variations, applications have the ability to trade resource usage for quality of service (QoS). QoS based resource management enables these tradeoffs in resource-constrained systems. In this paper we present our QoS approach, and we explore an integrated approach that addresses terminal and network resources, and takes power issues into account
Reduction techniques for synchronous dataflow graphs.
Get PDFThe Synchronous Dataflow (SDF) model of computation is popular for modelling the timing behaviour of real-time embedded hardware and software systems and applications. It is an essential ingredient of several automated design-flows and design-space exploration tools. The model can be analysed for throughput and latency properties. Although the SDF model is fairly simple, the analysis algorithms are often of high complexity and the models that need to be analysed may be fairly large. This paper introduces two graph transformations for reducing large SDF graphs into simpler, smaller ones that can be analysed more efficiently and give a conservative and often tight estimation of the timing of the original model and hence of the hard real-time system. We can make SDF based methods more efficient and prove that analyses that were done manually in an ad-hoc fashion in the past, can be done automatically and with guaranteed correctness. Additionally we introduce a novel conversion from SDF to Homogeneous SDF, a step applied in many analysis methods for SDF, which yields an up to 250X improvement on the number of actors, thus mitigating the problems with the size explosion observed in the traditional conversion
Embedded systems design issues in ambient intelligence
No full textThe vision of ambient intelligence opens a world of unprecedented ex.periences: the interaction of people with electronic devices is changed as context awareness, natural interfaces and ubiquitous availability of information are realized. We analyze the consequences of the ambient intelligence vision for embedded systems by mapping the involved technologies on a power-information graph. Based on differences in power consumption, three types of devices are introduced: the autonomous or microWau-node. the personal or milliWau-node and the static or Watt-node. Ambient intelligent functions are realized by a network of these devices with the computing, communication and interface electronics realized in Silicon IC technologies. The tri-partition of the ambient intelligence system hierarchy into microWatt nodes, milliWatt nodes, and Watt nodes introduces four major issues for embedded systems design
Preparation of heterogeneous networks for ambient intelligence
No full textAmbient Intelligence assumes the existence of ubiquitous networked computing.
Networking is supported in the home by a so-called home network. Currently,
the home network emerges from the purchase of a second PC in the home. Extending
the home network confronts the prospective buyer with a multitude of
standards. The more important representatives of these standards are discussed
and an integration path is described
- …
