Step by Step to Histories

  • Max Breitling
  • Jan Philipps
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


The behavior of reactive systems is typically specified by state machines. This results in an operational description of how a system produces its output. An alternative and more abstract approach is to just specify the relation between the input and output histories of a system. In this work, we propose a way to combine state-based and history-based specifications: Abstract communication history properties of system components can be derived from temporal logic properties of state machines. The history properties can then be used to deduce global properties of a complete system.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    N. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H. B. Sipma, and T. E. Uribe. STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems. In CAV’96. Lecture Notes in Computer Science 1102, pages 415–418, 1996.Google Scholar
  2. 2.
    M. Breitling and J. Philipps. Black Box Views of State Machines. Technical Report TUM-I9916, Institut für Informatik, Technische Universität München, 1999.Google Scholar
  3. 3.
    J. D. Brock and W. B. Ackermann. Scenarios: A model of nondeterministic computation. In J. Diaz and I. Ramos, editors, Lecture Notes in Computer Science 107, pages 225–259, 1981.Google Scholar
  4. 4.
    I. A. Browne, Z. Manna, and H. B. Sipma. Generalized temporal verification diagrams. In Lecture Notes in Computer Science 1026, pages 484–498, 1995.Google Scholar
  5. 5.
    M. Broy. Functional specification of time sensitive communicating systems. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Models, Formalism, Correctness. Lecture Notes in Computer Science 430, pages 153–179. Springer, 1990.Google Scholar
  6. 6.
    M. Broy. From states to histories. In Engineering Theories of Software Construction. NATO Science Series F, Marktoberdorf Summer School, 2000. To be published.Google Scholar
  7. 7.
    M. Broy, F. Dederichs, C. Dendorfer, M. Fuchs, T. F. Gritzner, and R. Weber. The Design of Distributed Systems: An Introduction to Focus—Revised Version. Technical Report TUM-I9202-2, Institut für Informatik, Technische Universität München, 1993.Google Scholar
  8. 8.
    M. Broy, F. Huber, B. Paech, B. Rumpe, and K. Spies. Software and system modeling based on a unified formal semantics. In M. Broy and B. Rumpe, editors, Requirements Targeting Software and Systems Engineering, International Workshop RTSE’97. Lecture Notes in Computer Science 1526. Springer, 1998.Google Scholar
  9. 9.
    F. Huber, B. Schätz, A. Schmidt, and K. Spies. Autofocus—a tool for distributed systems specification. In Proceedings FTRTFT’96 — Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science 1135, 1996.Google Scholar
  10. 10.
    L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages, 6(3):872–923, May 1994.CrossRefGoogle Scholar
  11. 11.
    Z. Manna and A. Pnueli. Models for reactivity. Acta Informatica, 30:609–678, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    L. C. Paulson. Logic and Computation. Cambridge University Press, 1987.Google Scholar
  13. 13.
    L. C. Paulson. Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science 828. Springer, 1994.zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Max Breitling
    • 1
  • Jan Philipps
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchenGermany

Personalised recommendations