Formal Development of a Network-Centric RTOS: Software Engineering for Reliable Embedded Systems

✍ Scribed by Eric Verhulst, Raymond T. Boute, José Miguel Sampaio Faria, Bernhard H.C. Sputh, Vitaliy Mezhuyev (auth.)

• Publisher: Springer US
• Year: 2011
• Tongue: English
• Leaves: 238
• Edition: 1
• Category: Library

✦ Synopsis

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 and higher performance. This methodology is unique because it covers the full range of product development, from requirements and specifications to the final execution platform. It is compatible with safety related engineering standards, such as IEC61508.

• Uses formal methods to develop Network-centric Real-time Operating Systems

• Unified Semantics provides a solid base for model driven systems development and can be tuned to an application-specific, concurrent programming paradigm

• Methods presented enable model-driven, high-reliability, high-performance software & systems engineering

• Compatible with International Electrotechnical Commission (IEC) 61508, the standard governing functional safety of programmable electronic systems.

✦ Table of Contents

Front Matter....Pages i-xvii
Front Matter....Pages 1-1
Introduction: OpenComRTOS Role in a Unified Systems Engineering Methodology....Pages 3-14
Requirements and Specifications for the OpenComRTOS Project....Pages 15-41
Front Matter....Pages 43-43
The Choice of TLA + /TLC: Comparing Formal Methods....Pages 45-72
Basic Formal Specification in TLA + ....Pages 73-86
Front Matter....Pages 87-87
Formal Modelling of the RTOS Entities....Pages 89-105
Final Architecture of the RTOS....Pages 107-119
Task Interaction Models in OpenComRTOS....Pages 121-131
Results: Code Size and Performance....Pages 133-140
Front Matter....Pages 141-141
OpenComRTOS-Suite 1.3 Usage Tutorial....Pages 143-168
Foundations for TLA + and Temporal Logic....Pages 169-197
Comparision of Formal Methods....Pages 199-210
Back Matter....Pages 211-219

✦ Subjects

Circuits and Systems; Computer-Aided Engineering (CAD, CAE) and Design