{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T06:43:33Z","timestamp":1775457813777,"version":"3.50.1"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,7,1]],"date-time":"2009-07-01T00:00:00Z","timestamp":1246406400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2009,7]]},"abstract":"<jats:p>\n            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\n            <jats:italic>transactions<\/jats:italic>\n            , and the structural relations are captured via class diagrams. The key feature of our approach is that our execution semantics leads to an\n            <jats:italic>abstract<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.1145\/1538942.1538943","type":"journal-article","created":{"date-parts":[[2009,7,28]],"date-time":"2009-07-28T12:43:55Z","timestamp":1248785035000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Interacting process classes"],"prefix":"10.1145","volume":"18","author":[{"given":"Ankit","family":"Goel","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abhik","family":"Roychoudhury","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. S.","family":"Thiagarajan","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,7,30]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"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","volume":"1055","author":"Alur R.","unstructured":"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. 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."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(00)00004-7"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_6_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 2000. Model Checking. MIT Press Cambridge.  Clarke E. M. Grumberg O. and Peled D. A. 2000. Model Checking. MIT Press Cambridge."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011227529550"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734088"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134328"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.596624"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1033228"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Harel D. and Marelly R. 2003. Come Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer-Verlag Berlin Germany.   Harel D. and Marelly R. 2003. Come Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-3-642-19029-2"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_14_1","volume-title":"Modeling a Simple Telephone Switch. The SPIN Model Checker","author":"Holzmann G.","unstructured":"Holzmann , G. 2004. Modeling a Simple Telephone Switch. The SPIN Model Checker . Addison-Wesley , Reading, Chapter 14. Holzmann, G. 2004. Modeling a Simple Telephone Switch. The SPIN Model Checker. Addison-Wesley, Reading, Chapter 14."},{"key":"e_1_2_1_15_1","unstructured":"Hopcroft J. E. and Ullman J. D. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley Reading.   Hopcroft J. E. and Ullman J. D. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley Reading."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625968"},{"key":"e_1_2_1_17_1","volume-title":"Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use","author":"Jensen K.","unstructured":"Jensen , K. 1995. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use . Vol. 1 . Springer-Verlag , Berlin, Germany . Jensen, K. 1995. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Vol. 1. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_18_1","volume-title":"MEMOCODE '04: Proceedings of the Second ACM and IEEE International Conference on Formal Methods and Models for Codesign. 161--168","author":"Lee E.","unstructured":"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 . 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."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_20_1","unstructured":"Murphi. 2005. Murphi description language and verifier. http:\/\/verify.stanford.edu\/dill\/murphi.html.  Murphi. 2005. Murphi description language and verifier. http:\/\/verify.stanford.edu\/dill\/murphi.html."},{"key":"e_1_2_1_21_1","unstructured":"OCaml. 2005. The OCaml programming language. http:\/\/caml.inria.fr\/ocaml\/index.en.html.  OCaml. 2005. The OCaml programming language. http:\/\/caml.inria.fr\/ocaml\/index.en.html."},{"key":"e_1_2_1_22_1","volume-title":"CAV'02: Proceedings of the 14th International Conference on Computer Aided Verification, E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science","volume":"2404","author":"Pnueli A.","unstructured":"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. 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."},{"key":"e_1_2_1_23_1","volume-title":"ACSD '03: Proceedings of the 3rd International Conference on the Application of Concurrency to System Design. IEEE Computer Society Press, Los Alamitos, 157","author":"Roychoudhury A.","unstructured":"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 . 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."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/646905.710490"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/587051.587077"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-002-0002-x"},{"key":"e_1_2_1_27_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"3057","author":"Wang T.","unstructured":"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. 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."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1024764232069"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1538942.1538943","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1538942.1538943","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:54Z","timestamp":1750278414000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1538942.1538943"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,7]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,7]]}},"alternative-id":["10.1145\/1538942.1538943"],"URL":"https:\/\/doi.org\/10.1145\/1538942.1538943","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,7]]},"assertion":[{"value":"2006-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}