Real-time systems need to react to certain input stimuli
within given time bounds. For example, an airbag in a car
has to unfold within 300 milliseconds in a crash. There are
many embedded safety-critical applications and each requires
real-time specification techniques. This text introduces three
of these techniques, based on logic and automata: duration
calculus, timed automata, and PLC-automata. The techniques are
brought together to form a seamless design flow, from real-time
requirements specified in the duration calculus; via designs
specified by PLC-automata; and into source code for hardware
platforms of embedded systems. The syntax, semantics, and proof
methods of the specification techniques are introduced; their
most important properties are established; and real-life examples
illustrate their use. Detailed case studies and exercises
conclude each chapter. Ideal for students of real-time systems
or embedded systems, this text will also be of great interest
to researchers and professionals in transportation and automation.
Describes real-time systems formally at the levels of
requirements, design specifications, and programs
Practical aspects are supported by tools that are freely
available on the web
Introduces automatic verification (model checking) methods for
design specifications against real-time requirements
Gives automatic translation functions of design specifications to
real-time programs
| Table of Contents |
| | Preface |
| | Acknowledgements |
| | List of symbols |
| 1 | Introduction |
| 2 | Duration Calculus |
| 3 | Properties and subsets of DC |
| 4 | Timed automata |
| 5 | PLC-Automata |
| 6 | Automatic verification |
| | Notations |
| | Bibliography |
| | Index |
