Modelling statecharts behaviour in a fully abstract way

  • C. Huizing
  • R. Gerth
  • W. P. de Roever
Parallelism And Concurrency
Part of the Lecture Notes in Computer Science book series (LNCS, volume 299)


We present a denotational, strictly syntax-directed, semantics for Statecharts, a graphical, mixed specification/programming language for real-time, developed by Harel [H]. This requires first of all defining a proper syntax for the graphical language. Apart from more conventional syntactical operators and their semantic counterparts, we encounter unconventional ones, dealing with the typical graphical structure of the language. The synchronous nature of Statecharts makes special demands on the semantics, especially with respect to the causal relation between simultaneous events, and requires a refinement of our techniques for obtaining a denotational semantics for OCCAM [HGR]. We prove that the model is fully abstract with respect to some natural notion of observable behaviour. The model presented will serve as a basis for a further study of specification and proof systems within the ESPRIT-project DESCARTES.


Operational Semantic Observable Behaviour Denotational Semantic Outgoing Transition Compositional Semantic 
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.


  1. [B]
    Berry G., Cosserat L. (1985), The Synchronous Programming Language ESTEREL and its Mathematical Semantics, in "Proc. CMU Seminar on Concurrency", LNCS 197, pp. 389–449, Springer-Verlag, New York.Google Scholar
  2. [BCH]
    Bergerand J.-L., Caspi P., Halbwachs N. (1985), Outline of a real-time dataflow language, in "Proc. IEEE-CS Real-Time systems Symposium", San Diego.Google Scholar
  3. [DD]
    Damm W., Döhmen G. (1987), An axiomatic approach to the specification of distributed computer architectures, in "Proc. PARLE Parallel Architectures and Languages Europe, Vol I", LNCS 258, Springer Verlag, Berlin.Google Scholar
  4. [G]
    Gonthier G., (1988), Ph.D. Thesis, Institute Nationale de Récherche en Informatique et en Automatique, Sophia-Antipolis, to appear.Google Scholar
  5. [GB]
    Gerth R., Boucher A., A Timed Failures Model for Extended Communicating Processes (1986), in "Proc. 14th Colloquium Automata, Languages and Programming ICALP", LNCS 267, pp. 95–114, Springer Verlag, Berlin.Google Scholar
  6. [GBBG]
    Le Guernic P., Beneviste A., Bournal P., Ganthier T. (1985), SIGNAL: A Data Flow Oriented Language For Signal Processing, IRISA Report 246, IRISA, Rennes, France.Google Scholar
  7. [H]
    Harel D. (1987), Statecharts: A visual Approach to Complex Systems, Science of Computer Programming, Vol. 8-3, pp. 389–449, pp. 231–274.Google Scholar
  8. [HePl]
    Hennessy M., Plotkin G. (1979), Full Abstraction for a Simple Programming Language, in "Proc. Math. Foundat. of Comput. Science", LNCS 74, pp. 108–120, Springer Verlag, New York.Google Scholar
  9. [HGR]
    Huizing C., Gerth R., De Roever W.P., (1987), Full Abstraction of a Real-Time Denotational Semantics for an OCCAM-like language, in "Proc. 14th ACM Symposium on Principles of Programming Languages POPL", pp. 223–237.Google Scholar
  10. [Ho]
    Hooman J. (1987), A compositional proof theory for real-time distributed message passing, in "Proc. PARLE Parallel Architectures and Languages Europe, Vol II", LNCS 259, pp. 315–332.Google Scholar
  11. [HP]
    Harel D., Pnueli A. (1985), On the Development of Reactive Systems, Logic and Models of Concurrent Systems, in "Proc. of the NATO Advanced Study Institute on Logics and Models for Verification and Specification of Concurrent Systems", NATO ASI Series F, Vol. 13, pp. 477–498 Springer Verlag, Berlin.Google Scholar
  12. [HPSS]
    Harel D., Pnueli A., Pruzan-Schmidt J., Sherman R. (1987), On the Formal Semantics of Statecharts, in "Proc. Symposion on Logic in Computer Science (LICS)", pp. 54–64.Google Scholar
  13. [HU]
    Hopcroft J.E., Ullman J.D. (1979), Introduction to automata theory, languages, and computation, Addison-Wesley, Reading.Google Scholar
  14. [K&]
    Koymans R., Shyamasundar R.K., De Roever W.P., Gerth R., Arun-Kumar S. (1988), Compositional Semantics for Real-Time Distributed Computing, Information and Control, to appear.Google Scholar
  15. [M]
    Mazurkiewicz A., Proving algorithms by tail functions, Information and Control, 18, (1971), pp. 220–226.Google Scholar
  16. [SM]
    Salwicki A., Müldner T. (1981), On the Algorithmic Properties of Concurrent Programs, in "Proc. Logic of Programs", LNCS 125, Springer Verlag, New York.Google Scholar
  17. [SW]
    Strachey C., Wadsworth C.P., Continuations: A Mathematical Semantics for Handling Full Jumps, Technical Monograph PRG-11, Oxford University Computing Laboratory, Oxford.Google Scholar
  18. [Z]
    Zwiers J. (1988), Compositionality and dynamic networks of processes: Investigating verification systems for DNP, Ph.D. Thesis, Eindhoven University of Technology, to appear.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • C. Huizing
    • 1
  • R. Gerth
    • 1
  • W. P. de Roever
    • 1
  1. 1.Department of Mathematics and Computing ScienceEindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations