Formal Specification

  • Doron A. Peled
Part of the Texts in Computer Science book series (TCS)


Most software projects are developed over a period of several months or even years. Over its lifetime, a software product is often updated, new features are added, and adjustments are made at the request of the users. A complete system may include millions of lines of code. It is sometimes developed and maintained by hundreds of people, located in different places. A software system may consist of numerous parts, each responsible for performing some predefined tasks. Interfaces through which the different parts can interact with each other need to be defined. The right use of the interfaces between the different components is important for integrating them into a system that operates correctly.


Order Logic Traffic Light Critical Section Mutual Exclusion Linear Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Further Reading

A book on software specification is

  1. V. S. Alagar, K. Periyasamy, Specification of Software Systems, Springer-Verlag, 1998.Google Scholar
  2. Two surveys on Büchi automata and monadic second order logic by Wolfgang Thomas areGoogle Scholar
  3. W. Thomas, Automata on infinite objects, in Handbook of Theoretical Computer Science, vol. B, J. van Leeuwen (ed)., Elsevier, (1990) 133–191.Google Scholar
  4. W. Thomas, Languages, Automata, and Logic, in Handbook of Formal Language Theory,G. Rozenberg, A. Salomaa, (eds.), Volume 3, Springer-Verlag, 389–455.Google Scholar

The temporal approach for specification is extensively described in the following books:

  1. Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1991.Google Scholar
  2. F. Kröger, Temporal Logic of Programs, EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1992.Google Scholar

A more general perspective on temporal logic can be found in the following survey paper:

  1. E. A. Emerson, Temporal and Modal Logic, in Handbook of Theoretical Computer Science, vol. B, J. van Leeuwen (ed.), Elsevier, (1990), 995–1072.Google Scholar

Copyright information

© Lucent Technologies 2001

Authors and Affiliations

  • Doron A. Peled
    • 1
  1. 1.Computing SciencesBell Labs/Lucent TechnologiesMurray HillUSA

Personalised recommendations