Interacting process classes

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Interacting process classes

Full text

Pdf (667 KB)

Source

ACM Transactions on Software Engineering and Methodology (TOSEM) archive
Volume 18 , Issue 4 (July 2009) table of contents

Article No. 13

Year of Publication: 2009

ISSN:1049-331X

Authors

Ankit Goel	National University of Singapore, Singapore
Abhik Roychoudhury	National University of Singapore, Singapore
P. S. Thiagarajan	National University of Singapore, Singapore

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 37, Downloads (12 Months): 147, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1538942.1538943 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Rajeev Alur , Gerard J. Holzmann , Doron Peled, An Analyser for Mesage Sequence Charts, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.35-48, March 27-29, 1996
	2	Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
	3	Basten, T. and van der Aalst, W. 2001. Inheritance of behavior. J. Log. Algebr. Program. 47, 2, 47--145.
	4	Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003 [doi>10.1145/876638.876643]
	5	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
	6	Clarke, E. M., Grumberg, O., and Peled, D. A. 2000. Model Checking. MIT Press, Cambridge.
	7	Werner Damm , David Harel, LSCs: Breathing Life into Message Sequence Charts, Formal Methods in System Design, v.19 n.1, p.45-80, July 2001 [doi>10.1023/A:1011227529550]
	8	Giorgio Delzanno, Automatic Verification of Parameterized Cache Coherence Protocols, Proceedings of the 12th International Conference on Computer Aided Verification, p.53-68, July 15-19, 2000
	9	Ankit Goel , Sun Meng , Abhik Roychoudhury , P. S. Thiagarajan, Interacting process classes, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134328]
	10	David Harel , Eran Gery, Executable Object Modeling with Statecharts, Computer, v.30 n.7, p.31-42, July 1997 [doi>10.1109/2.596624]
	11	David Harel , Orna Kupferman, On Object Systems and Behavioral Inheritance, IEEE Transactions on Software Engineering, v.28 n.9, p.889-903, September 2002 [doi>10.1109/TSE.2002.1033228]
	12	David Harel , Rami Marelly, Come, Let's Play: Scenario-Based Programming Using LSC's and the Play-Engine, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
	13	Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
	14	Holzmann, G. 2004. Modeling a Simple Telephone Switch. The SPIN Model Checker. Addison-Wesley, Reading, Chapter 14.
	15	John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	16	C. Norris Ip , David L. Dill, Better verification through symmetry, Formal Methods in System Design, v.9 n.1-2, p.41-75, Aug. 1996 [doi>10.1007/BF00625968]
	17	Kurt Jensen, Coloured Petri nets: basic concepts, analysis methods and practical use, vol. 2, Springer-Verlag, London, 1995
	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	Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
	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	Amir Pnueli , Jessie Xu , Lenore D. Zuck, Liveness with (0, 1, infty)-Counter Abstraction, Proceedings of the 14th International Conference on Computer Aided Verification, p.107-122, July 27-31, 2002
	23	Abhik Roychoudhury , P. S. Thiagarajan, Communicating Transaction Processes, Proceedings of the Third International Conference on Application of Concurrency to System Design, p.157, June 18-20, 2003
	24	Bran Selic, Using UML for Modeling Complex Real-Time Systems, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.250-260, June 01, 1998
	25	Bikram Sengupta , Rance Cleaveland, Triggered message sequence charts, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587077]
	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	Heike Wehrheim, Behavioral Subtyping Relations for Active Objects, Formal Methods in System Design, v.23 n.2, p.143-170, September 2003 [doi>10.1023/A:1024764232069]