And/Or Hierarchies and Round Abstraction

  • 1Radu Grosu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)


Sequential and parallel composition are the most fundamental operators for incremental construction of complex concurrent systems. They reflect the temporal and respectively the spatial properties of these systems. Hiding temporal detail like internal computation steps supports temporal scalability and may turn an asynchronous system to a synchronous one. Hiding spatial detail like internal variables supports spatial scalability and may turn a synchronous system to an asynchronous one. In this paper we show on hand of several examples that a language explicitly supporting both sequential and parallel composition operators is a natural setting for designing heterogeneous synchronous and asynchronous systems. The language we use is Shrm, a visual language that backs up the popular and/or hierarchies of statecharts with a well defined compositional semantics.


Model Check Global Variable Exit Point Parallel Composition Reactive Module 
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. [AG00]
    R. Alur and R. Grosu. Modular refinement of hierarchic reactive machines. In Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages, pages 390–402, 2000.Google Scholar
  2. [AGM00]
    R. Alur, R. Grosu, M. McDougall. Efficient Reachability Analysis of Hierarchical Reactive Machines. In Proceedings of the 12th Conference on Computer Aided Verification, Chicago, USA, 2000.Google Scholar
  3. [AH99]
    R. Alur and T.A. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7–48, 1999.CrossRefMathSciNetGoogle Scholar
  4. [AHM+98]_R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In Proceedings of the 10th International Conference on Computer Aided Verification, LNCS 1427, pages 516–520. Springer-Verlag, 1998.CrossRefGoogle Scholar
  5. [AKS83]
    S. Aggarwal, R.P. Kurshan, and D. Sharma. A language for the specification and analysis of protocols. In IFIP Protocol Specification, Testing, and Verification III, pages 35–50, 1983.Google Scholar
  6. [AKY99]
    R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. In Automata, Languages and Programming, 26th International Colloquium, pages 169–178. 1999.Google Scholar
  7. [AY98]
    R. Alur and M. Yannakakis. Model checking of hierarchical state machines. In Proceedings of the Sixth ACM Symposium on Foundations of Software Engineering, pages 175–188. 1998.Google Scholar
  8. [BHSV+96]_R. Brayton, G. Hachtel, A. Sangiovanni-Vincentell, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In Proceedings of the Eighth Conference on Computer Aided Verification, LNCS 1102, pages 428–432. 1996.Google Scholar
  9. [BJR97]
    G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997.Google Scholar
  10. [BLA+99]_G. Behrmann, K. Larsen, H. Andersen, H. Hulgaard, and J. Lind-Nielsen. Verification of hierarchical state/event systems using reusability and compositionality. In TAC AS’ 99: Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Software, 1999.Google Scholar
  11. [CAB+98]_W. Chan, R. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498–519, 1998.CrossRefGoogle Scholar
  12. [CE81]
    E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pages 52–71. Springer-Verlag, 1981.CrossRefGoogle Scholar
  13. [CK96]
    E.M. Clarke and R.P. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61–67, 1996.CrossRefGoogle Scholar
  14. [Har87]
    D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  15. [Hol91]
    G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.Google Scholar
  16. [Hol97]
    G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.CrossRefMathSciNetGoogle Scholar
  17. [JM87]
    F. Jahanian and A.K. Mok. A graph-theoretic approach for timing analysis and its implementation. IEEE Transactions on Computers, C-36(8):961–975, 1987.CrossRefGoogle Scholar
  18. [LHHR94]
    N.G. Leveson, M. Heimdahl, H. Hildreth, and J.D. Reese. Requirements specification for process control systems. IEEE Transactions on Software Engineerings, 20(9), 1994.Google Scholar
  19. [McM93]
    K. McMillan. Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, 1993.Google Scholar
  20. [PD96]
    L. Peterson and B. Davie. Computer Networks: A Systems Approach. Morgan Kaufmann, 1996.Google Scholar
  21. [Pet81]
    G. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3), 1981.Google Scholar
  22. [QS82]
    J.P. Queille and J. Sifakis. Specification and verification of concurrent programs in CESAR. In Proceedings of the Fifth International Symposium on Programming, LNCS 137, pages 195–220. Springer-Verlag, 1982.Google Scholar
  23. [SGW94]
    B. Selic, G. Gullekson, and P.T. Ward. Real-time object oriented modeling and design. J. Wiley, 1994.Google Scholar
  24. [Ver]
    IEEE Standard 1364-1995. Verilog Hardware Description Language Reference Manual, 1995.Google Scholar
  25. [Vhdl]
    IEEE Standard 1076-1993. VHDL Language Reference Manual, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • 1Radu Grosu
    • 1
  1. 1.Department of Computer and Information ScienceUniversity of PennsylvaniaUSA

Personalised recommendations