Interacting process classes

Abstract

Many reactive control systems consist of classes of active objects involving both intraclass interactions (i.e., objects belonging to the same class interacting with each other) and interclass interactions. Such reactive control systems appear in domains such as telecommunication, transportation and avionics. In this article, we propose a modeling and simulation technique for interacting process classes. Our modeling style uses standard notations to capture behavior. In particular, the control flow of a process class is captured by a labeled transition system, unit interactions between process objects are described as transactions, and the structural relations are captured via class diagrams. The key feature of our approach is that our execution semantics leads to an abstract simulation technique which involves (i) grouping together active objects into equivalence classes according their potential futures, and (ii) keeping track of the number of objects in an equivalence class rather than their identities. Our simulation strategy is both time and memory efficient and we demonstrate this on well-studied nontrivial examples of reactive systems. We also present a case study involving a weather-update controller from NASA to demonstrate the use of our simulator for debugging realistic designs.

References

1. Alur, R., Holzmann, G., and Peled, D. 1996. An analyzer for message sequence charts. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), T. Margaria and B. Steffen, Eds. Lecture Notes in Computer Science, vol. 1055. Springer, Berlin/Heidelberg, Germany, 35--48.
2. Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. K. 2001. Automatic predicate abstraction of c programs. In PLDI '01: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, New York, 203--213.
3. Basten, T. and van der Aalst, W. 2001. Inheritance of behavior. J. Log. Algebr. Program. 47, 2, 47--145.
4. Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2003. Counter-example-guided abstraction refinement for symbolic model checking. J. Assoc. Comput. Mach. 50, 5, 752--794.
5. Clarke, E. M., Grumberg, O., and Long, D. E. 1994. Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16, 5, 1512--1542.
6. Clarke, E. M., Grumberg, O., and Peled, D. A. 2000. Model Checking. MIT Press, Cambridge.
7. Damm, W. and Harel, D. 2001. LSCs: Breathing life into message sequence charts. Form. Meth. Syst. Des. 19, 1, 45--80.
8. Delzanno, G. 2000. Automatic verification of parameterized cache coherence protocols. In CAV '00: Proceedings of the 12th International Conference on Computer-Aided Verification, E. A. Emerson and A. P. Sistla, Eds. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, London, U.K., 53--68.
9. Goel, A., Meng, S., Roychoudhury, A., and Thiagarajan, P. S. 2006. Interacting process classes. In ICSE '06: Proceeding of the 28th International Conference on Software Engineering (Shanghai, China). ACM Press, New York, 302--311.
10. Harel, D. and Gery, E. 1997. Executable object modeling with statecharts. IEEE Comput. 30, 7, 31--42.
11. Harel, D. and Kupferman, O. 2002. On object systems and behavioral inheritance. IEEE Trans. Softw. Eng. 28, 9, 889--903.
12. Harel, D. and Marelly, R. 2003. Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer-Verlag, Berlin, Germany.
13. Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages (Portland, Oregon). ACM Press, New York, 58--70.
14. Holzmann, G. 2004. Modeling a Simple Telephone Switch. The SPIN Model Checker. Addison-Wesley, Reading, Chapter 14.
15. Hopcroft, J. E. and Ullman, J. D. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading.
16. Ip, C. and Dill, D. 1996. Better verification through symmetry. Form. Meth. Syst. Des. 9, 2, 41--75.
17. Jensen, K. 1995. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Vol. 1. Springer-Verlag, Berlin, Germany.
18. Lee, E. and Neuendorffer, S. 23-25 June 2004. Classes and subclasses in actor-oriented design. In MEMOCODE '04: Proceedings of the Second ACM and IEEE International Conference on Formal Methods and Models for Codesign. 161--168.
19. Liskov, B. H. and Wing, J. M. 1994. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16, 6, 1811--1841.
20. Murphi. 2005. Murphi description language and verifier. http://verify.stanford.edu/dill/murphi.html.
21. OCaml. 2005. The OCaml programming language. http://caml.inria.fr/ocaml/index.en.html.
22. Pnueli, A., Xu, J., and Zuck, L. D. 2002. Liveness with (0, 1, infty)-counter abstraction. In CAV'02: Proceedings of the 14th International Conference on Computer Aided Verification, E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, London, U.K., 107--122.
23. Roychoudhury, A. and Thiagarajan, P. S. 2003. Communicating transaction processes. In ACSD '03: Proceedings of the 3rd International Conference on the Application of Concurrency to System Design. IEEE Computer Society Press, Los Alamitos, 157.
24. Selic, B. 1998. Using UML for modeling complex real-time systems. In LCTES '98: Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, F. Mueller and A. Bestavros, Eds. Lecture Notes in Computer Science, vol. 1474. Springer-Verlag, London, U.K., 250--260.
25. Sengupta, B. and Cleaveland, R. 2002. Triggered message sequence charts. In SIGSOFT '02/FSE-10: Proceedings of the 10th ACM SIGSOFT Symposium on Foundations of Software Engineering (Charleston, SC). ACM Press, New York, 167--176.
26. Stevens, P. 2002. On the interpretation of binary associations in the Unified Modeling Language. J. Softw. Syst. Model. 1, 1, 68--79.
27. Wang, T., Roychoudhury, A., Yap, R., and Choudhary, S. 2004. Symbolic execution of behavioral requirements. In Practical Aspects of Declarative Languages, B. Jayaraman, Ed. Lecture Notes in Computer Science, vol. 3057. Springer, Berlin/Heidelberg, Germany, 178--192.
28. Wehrheim, H. 2003. Behavioral subtyping relations for active objects. Form. Meth. Sys. Des. 23, 2, 143--170.

Index Terms

• Software and its engineering

  • Software creation and management

    • Designing software

      • Requirements analysis

  • Software organization and properties

    • Software system structures

      • Software system models

        • State systems