Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2011 | Buch

Introduction: OpenComRTOS Role in a Unified Systems Engineering Methodology Kapitel lesen Erstes Kapitel lesen

Formal Development of a Network-Centric RTOS

Software Engineering for Reliable Embedded Systems

verfasst von: Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H.C. Sputh, Vitaliy Mezhuyev

Verlag: Springer US

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

Many systems, devices and appliances used routinely in everyday life, ranging from cell phones to cars, contain significant amounts of software that is not directly visible to the user and is therefore called "embedded". For coordinating the various software components and allowing them to communicate with each other, support software is needed, called an operating system (OS). Because embedded software must function in real time (RT), a RTOS is needed. This book describes a formally developed, network-centric Real-Time Operating System, OpenComRTOS. One of the first in its kind, OpenComRTOS was originally developed to verify the usefulness of formal methods in the context of embedded software engineering. Using the formal methods described in this book produces results that are more reliable while delivering higher performance. The result is a unique real-time concurrent programming system that supports heterogeneous systems with just 5 Kbytes/node. It is compatible with safety related engineering standards, such as IEC61508.

Inhaltsverzeichnis

Frontmatter

Trustworthy Embedded Systems

Frontmatter
Chapter 1. Introduction: OpenComRTOS Role in a Unified Systems Engineering Methodology
Abstract
OpenComRTOS is part of a systematic, formalised systems and software engineering methodology for embedded systems with a supporting environment and tools. While OpenComRTOS can be used independently of it, users will benefit from using the methodology in an integrated way. This methodology is characterised by two key concepts: unified semantics and interacting entities. When used in combination, they result in a better control of the engineering process leading to the development of systems and products. OpenComRTOS plays an important role in this approach as it is the system software layer allowing the mapping of the abstract interacting entities at the modeling level into concrete concurrent instances.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev
Chapter 2. Requirements and Specifications for the OpenComRTOS Project
Abstract
In this chapter, we discuss the requirements and specifications for the OpenComRTOS project from the point of view of its capabilities to support applications in meeting real-time requirements. As this is related to a distributed real-time operating system this is rather unique as most RTOS are designed for single processor systems and if not, they assume a shared memory architecture whereby the address space is global. OpenComRTOS on the other hand makes no such assumptions, but assumes that a processor has local memory and that the hardware allows to communicate somehow between the processors’ memory. It is a network model, but allowing to emulate it by shared memory if this is available. Hence the term “network-centric” RTOS. In this context, we also explain the CSP background that is still present in the conceptual design of OpenComRTOS.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev

Formal Modeling Fundamentals

Frontmatter
Chapter 3. The Choice of TLA+/TLC: Comparing Formal Methods
Abstract
This book provides a thorough description of OpenComRTOS and of the formal models built for its implementation. Such models were written in TLA +  and verified with the TLC model checker. The choice of TLA + /TLC was one of the fundamental initial decisions of the project. In effect, over the last years, several languages, techniques, and tools have been developed and made available by the formal methods community. Typically, different formalisms are best suited for different domains of application, and their comparison is not straightforward. It can be a significantly subjective exercise. This chapter addresses this issue, describing the selection process followed in this project.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev
Chapter 4. Basic Formal Specification in TLA+
Abstract
Model checking (Clarke et al. 1999; Holzmann 2003b; Lamport 2002a) is a flexible and powerful technique for verifying systems formally with automated tools. In principle, it makes this task easy for the user: given a formal system description and certain conditions to be satisfied, the automated checker either confirms that the system satisfies the conditions, or provides a counterexample.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev

OpenComRTOS Design

Frontmatter
Chapter 5. Formal Modelling of the RTOS Entities
Abstract
This chapter describes the formal TLA + models of the OpenComRTOS Layer 1 Interaction Entities (L1-Entities). The L1-Entities represent the API (Application Programmer’s Interface) of OpenComRTOS used by the Task entities to build up the application. There are also so-called Layer 0 entities but these are not accessible to the user. The L1 Entities are also all derived from a common so-called Hub Entity. As we will see later, the L1-Entities represent services the operating system offers to the user. The L1-Entities names represent the type of service they provide.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev
Chapter 6. Final Architecture of the RTOS
Abstract
This chapter discusses the implementation architecture of OpenComRTOS. This is done by using a small test program, called theSemaphore Loop. It follows a top down approach by first explaining the Semaphore Loop itself, including a definition of the Semaphore in terms of OpenComRTOS. This is followed by an explanation of what happens when a Task sends a request to the OpenComRTOS Kernel, taking as example the signalling and testing of a Semaphore. This example then is extended to a system consisting of two processing nodes, connected via a link, each of which executing part of the Semaphore Loop example. While the logical behaviour is the same, the resulting changes in the execution are discussed.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev
Chapter 7. Task Interaction Models in OpenComRTOS
Abstract
Tasks in OpenComRTOS interact using an intermediate Hub entity. This way the interaction is decoupled from the tasks themselves. Different temporal semantics (waiting, non-waiting, and waiting with timeout) of tasks synchronization are formalised. Conclusions are drawn on correct usage confirming the correctness of the original CSP semantics.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev
Chapter 8. Results: Code Size and Performance
Abstract
We briefly show that the resulting architecture generates very small code (5 KB for the distributed version) resulting in better performance and better safety properties.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev

Appendix

Frontmatter
Appendix A. OpenComRTOS-Suite 1.3 Usage Tutorial
Abstract
The previous chapters of this book concentrated the theoretical foundations of OpenComRTOS and the formal modelling effort that was done in order to develop a trustworthy Real Time Operating System (RTOS). This chapter concentrates on the development of applications which utilise OpenComRTOS, as provided by OpenComRTOS-Suite 1.3. It is designed as a tutorial the reader can follow step by step. Section 9.1 gives a detailed introduction to OpenVE (the main development tool of the OpenComRTOS-Suite) to develop a Semaphore-loop executing on a single win32-node. The resulting project is then extended in Sect. 9.2 to utilise multiple nodes (MP), by introducing a second win32-node and connecting the two win32-nodes using TCP/IP. This illustrates how easy it is to construct distributed systems using the OpenComRTOS-Suite.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev
Appendix B. Foundations for TLA+ and Temporal Logic
Abstract
As mentioned in Chap. 4, mathematics is the main intellectual tool for the genuine systems designer. In particular, the user of automated model or proof checkers can benefit from mathematical reasoning about both the system descriptions (e.g. programs) and the conditions (e.g. invariants, temporal formulas) in various respects.
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev
Appendix C. Comparision of Formal Methods
Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H. C. Sputh, Vitaliy Mezhuyev
Backmatter
Metadaten
Titel
Formal Development of a Network-Centric RTOS
verfasst von
Eric Verhulst
Raymond T. Boute
José Miguel Sampaio Faria
Bernhard H.C. Sputh
Vitaliy Mezhuyev
Copyright-Jahr
2011
Verlag
Springer US
Electronic ISBN
978-1-4419-9736-4
Print ISBN
978-1-4419-9735-7
DOI
https://doi.org/10.1007/978-1-4419-9736-4

Neuer Inhalt

    Bildnachweise