Series: Trends in Software

• OVERVIEW

  This book surveys the state-of-the-art techniques and the state-of-practice approaches in formal methods for real-time computing. There is growing recognition of the crucial role of timing in many computer systems, especially safety-critical systems. Moreover, the benefits of increasing the level of formalism, especially in the early stages of specification and design, has recently been demonstrated in a number of industrial-strength applications. This issue of the John Wiley Series on Software Trends focuses on the application of formal methods in the development of "hard" real-time systems, that is, systems that are required to satisfy critical timing requirements.

  The book consists of 10 chapters. The first chapter provides an overview of the leading specification languages, formal models, and analysis techniques for developing real-time systems. Each of the following chapters is written by experts in a particular method. Included are chapters on the Modechart language, the I/O Timed Automaton model, the Duration Calculus, Timed LOTOS, a real-time process algebra called the Algebra of Communicating Shared Resources, Timed Petri Nets, the real-time logic TRIO, automata-theoretic verification, symbolic model checking, and an end-to-end design methodology for guaranteeing requirements of real-time systems. The book uses a tutorial style and gives readers intuition about promising approaches and their practical impact through the use of examples. It is essential reading for students of formal methods and real-time system development, project managers considering the use of formal methods, and researchers interested in learning more about the major new formalisms for specifying and verifying real-time systems.

  BOOK INDEX CONTENTS OF THIS BOOK

• TABLE OF CONTENTS AND CONTRIBUTORS

• EXCERPT FROM THE BOOK PREFACE

• ORGANIZATION OF THE CHAPTERS

• ABSTRACTS