| 1. |
|
|
| 2. |
|
|
| 3. |
- Lundqvist, Kristina, et al.
(författare)
-
Non-Intrusive System-Level Fault Tolerance
- 2005
-
Ingår i: Lecture Notes in Computer Science, Volume 3555. ; , s. 156-166
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)
|
|
| 4. |
|
|
| 5. |
|
|
| 6. |
|
|
| 7. |
- Naeser, Gustaf, et al.
(författare)
-
Temporal Skeletons for Verifying Time
- 2005
-
Ingår i: Proceedings of the ACM SIGAda Annual International Conference; SIGAda. - : Association for Computing Machinery (ACM). - 1595931856 ; , s. 49-56
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- This paper presents an intermediate notation used in a framework for verification of real-time properties. The framework aims at overcoming the need for the framework user to have significant knowledge of the verification specific detail that formal verification at some level is bound to impose on a model. In order to accomplish this, model extraction from source code of an initial formal model, a timing skeleton, is made automatically. The model refinement needed to transform the temporal skeleton into a model that can be verified is not done immediately. This allows postponement of the abstraction and specialisation needed for the verification which further improves the readability of the skeleton. The purpose of the timing skeleton is that it easily can be validated to represent the source code it was created from. The timing skeleton is then automatically refined with verification detail, and then hidden for the user, transformed into the notation of a verification tool. This transformation is hidden from the user. In order to reduce the complexity of the application model the framework uses a formally verified run-time kernel with a clear separation from the application. The kernel supports preemption, dynamic priorities and multiple processors.
|
|
| 8. |
- Nordström, Susanna, 1975-
(författare)
-
Configurable Hardware Support for Single Processor Real-Time Systems
- 2008
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- This thesis describes a further development of a building block for programmable devices in embedded systems handling real-time functionality.Embedded systems are included in a variety of products within different technical areas such as industrial automation, consumer electronics, automotive industry, and communication-, and multimedia systems. Products ranging from trains and airplanes to microwave ovens and washing machines are controlled by embedded systems.Programmable devices constitute a part of these embedded systems. Today, a programmable device can include a complete system containing building blocks connected with each other via programs written using a hardware description language. The programmable devices can be programmed and changed over and over again and this flexibility makes it possible to explore how these building blocks can best be designed in relation to system requirements, before final implementation.This thesis describes a further development of a building block for programmable devices implemented in a non-traditional way, i.e., the implementation is written using both hardware description language and traditional software languages. This new building block handles real-time functionality in a non-traditional way that enables certain benefits, such as increased performance, predictability and less memory consumption. Using a non-traditional implementation also has its drawbacks, and e.g., extensions and adjustments can be hard to handle since modifications are required in both hardware and software programming languages.The new building block was investigated in order to see how it could be facilitated when used for real-time functionality. The configurability of the block was extended which enables further customization of the building block. This leads to the possibility to use the block within a wider spectrumof applications. It is also possible to reduce the size and cost of the final product since resource usage can be optimized.Furthermore, a mathematicalmodel estimating resource usage for real-time functionality has been developed. The model enables distinctive trade-offs comparisons, and guidance for system designers, when considering what type of real-time operating system to use in a certain design.
|
|
| 9. |
|
|
| 10. |
|
|
