Abstract interpretation of reactive systems

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Abstract interpretation of reactive systems

Full text

Pdf (501 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 19 , Issue 2 (March 1997) table of contents

Pages: 253 - 291

Year of Publication: 1997

ISSN:0164-0925

Authors

Dennis Dams	Eindhoven Univ. of Technology, Eindhoven, The Netherlands
Rob Gerth	Eindhoven Univ. of Technology, Eindhoven, The Netherlands
Orna Grumberg	Technion–Israel Institute of Technology, Haifa, Israel

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 13, Downloads (12 Months): 140, Citation Count: 49

Additional Information:

references cited by index terms review 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/244795.244800 What is a DOI?

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	R. J. R. Back , R. Kurki-Suonio, Decentralization of process nets with centralized control, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.131-142, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806716]
	2	Saddek Bensalem , Ahmed Bouajjani , Claire Loiseaux , Joseph Sifakis, Property Preserving Simulations, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.260-273, June 29-July 01, 1992
	3	A. Bouajjani , J.-C. Fernandez , N. Halbwachs , P. Raymond , C. Ratel, Minimal state graph generation, Science of Computer Programming, v.18 n.3, p.247-269, June 1992 [doi>10.1016/0167-6423(92)90018-7]
	4	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	5	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
	6	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]
	7	Rance Cleaveland , James Riely, Testing-Based Abstractions for Value-Passing Systems, Proceedings of the Concurrency Theory, p.417-432, August 22-25, 1994
	8	Rance Cleaveland , S. Purushothaman Iyer , Daniel Yankelevich, Optimality in Abstractions of Model Checking, Proceedings of the Second International Symposium on Static Analysis, p.51-63, September 25-27, 1995
	9	Rance Cleaveland , S. P Iyer , Daniel Yankelevich, Abstractions for Preserving All CTL* Formulae, North Carolina State University at Raleigh, Raleigh, NC, 1994
	10	Michael Codish , Moreno Falaschi , Kim Marriott, Suspension analyses for concurrent logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.649-686, May 1994 [doi>10.1145/177492.177656]
	11	Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
	12	Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
	13	Patrick Cousot , Rahida Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, v.13 n.2-3, p.103-179, July 1992 [doi>10.1016/0743-1066(92)90030-7]
	14	COUSOT, P. AND COUSOT, R. 1992b. Abstract interpretation frameworks. J. Logic Comput. 2, 4, 511-547.
	15	Mads Dam, CTL and ECTL as fragments of the modal &mgr;-calculus, Theoretical Computer Science, v.126 n.1, p.77-96, April 11, 1994 [doi>10.1016/0304-3975(94)90269-0]
	16	Werner Damm , Hardi Hungar , Peter Kelb , Rainer Schlör, Statecharts, Formal Development of Reactive Systems - Case Study Production Cell, p.131-149, January 1995
	17	Dennis Dams , Rob Gerth , Gert Döhmen , Ronald Herrmann , Peter Kelb , Hergen Pargmann, Model Checking Using Adaptive State and Data Abstraction, Proceedings of the 6th International Conference on Computer Aided Verification, p.455-467, June 21-23, 1994
	18	Dennis Dams , Orna Grumberg , Rob Gerth, Generation of Reduced Models for Checking Fragments of CTL, Proceedings of the 5th International Conference on Computer Aided Verification, p.479-490, June 28-July 01, 1993
	19	DAMS, D., GRUMBERG, O., AND GERTH, R. 1993b. Abstract interpretation of reactive systems: Abstractions preserving ACTL, ECTL and CTL*. Dept. of Mathematics and Computing Science, Eindhoven Univ. of Technology, Eindhoven, The Netherlands.
	20	DAMS, D., GRUMBERG, O., AND GERTH, R. 1995. Abstract interpretation of reactive systems: Preservation of CTL* Logic Group Preprint Series 132, Dept. of Philosophy, Utrecht Univ., Utrecht, The Netherlands. May. Also appeared as Computing Science Note 95/16, Dept. of Mathematics and Computing Science, Eindhoven Univ. of Technology.
	21	DAMS, D. R. 1996. Abstract interpretation and partition refinement for model checking. Ph.D. thesis, Eindhoven Univ. of Technology, Eindhoven, The Netherlands.
	22	Nicoletta De Francesco , Alessandro Fantechi , Stefania Gnesi , Paola Inverardi, Model Checking of Non-Finite State Processes by Finite Approximations, Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.195-215, May 19-20, 1995
	23	David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, MIT Press, Cambridge, MA, 1989
	24	E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
	25	GINZBURG, A. 1968. Algebraic Theory of Automata. ACM Monograph Series. Academic Press, New York/London.
	26	Susanne Graf, Verification of a Distributed Cache Memory by Using Abstractions, Proceedings of the 6th International Conference on Computer Aided Verification, p.207-219, June 21-23, 1994
	27	Susanne Graf , Claire Loiseaux, A Tool for Symbolic Program Verification and Abstration, Proceedings of the 5th International Conference on Computer Aided Verification, p.71-84, June 28-July 01, 1993
	28	David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
	29	Matthew Hennessy , Robin Milner, On Observing Nondeterminism and Concurrency, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.299-309, July 14-18, 1980
	30	KELB, P. 1994. Model checking and abstraction: A framework preserving both truth and failure information. Carl yon Ossietzky Univ. of Oldenburg, Oldenburg, Germany. Unpublished note.
	31	KELB, P. 1995. Abstraktionstechniken fiir automatische verifikationsmethoden. Ph.D. thesis, Carl yon Ossietzky Univ. of Oldenburg, Oldenburg, Germany.
	32	KELB, P., DAMS, D., AND GERTH, R. 1995. Efficient symbolic model checking of the full >- calculus using compositional abstractions. Computing Science Rep. 95/31, Eindhoven Univ. of Technology, Eindhoven, The Netherlands. Oct.
	33	KOZEN, D. 1983. Results on the propositional #-calculus. Theor. Comput. Sci. 27, 333-354.
	34	KRIPKE, S. 1963. A semantical analysis of modal logic I: Normal modal propositional calculi. Zeitschrift fiir Mathematische Logik und Grundlagen der Mathematik 9, 67-96.
	35	R. P. Kurshan, Analysis of discrete event coordination, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.414-453, May 1990, Mook, The Netherlands
	36	Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
	37	K. G. Larsen, Modal specifications, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.232-246, February 1990, Grenoble, France
	38	LARSEN, K. G. AND THOMSEN, B. 1988. A modal process logic. In the 1988 IEEE Symposium on Logic in Computer Science. IEEE Computer Society, Washington, D.C., 203-210.
	39	Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
	40	LOISEAUX, C. 1994. V6rification symbolique de syst~mes r6actifs g l'aide d'abstractions. Ph.D. thesis, Universit6 Joseph Fourier- Grenoble I, Grenoble, France.
	41	C. Loiseaux , S. Graf , J. Sifakis , A. Bouajjani , S. Bensalem, Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, v.6 n.1, p.11-44, Jan. 1995 [doi>10.1007/BF01384313]
	42	David Esley Long, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
	43	Kim Marriott, Frameworks for abstract interpretation, Acta Informatica, v.30 n.2, p.103-129, March 1993 [doi>10.1007/BF01178576]
	44	MILNER, R. 1971. An algebraic definition of simulation between programs. In the 2nd International Joint Conference on Artificial Intelligence. British Computer Society, London, U.K., 481-489.
	45	David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
	46	Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
	47	SIFAKIS, J. 1982. Property preserving homomorphisms and a notion of simulation for transition systems. Rapport de Recherche 332, IMAG, Grenoble, France. Nov.
	48	Joseph Sifakis, Property Preserving Homomorphisms of Transition Systems, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.458-473, June 06-08, 1983
	49	VAN BENTHEM, J., VAN EIJCK, J., AND STEBLETSOVA, V. 1994. Modal logic, transition systems and processes. J. Logic Comput. 4, 5, 811-855.
	50	VARDI, M. Y. AND WOLPER, P. 1986. An automata-theoretic approach to automatic program verification (preliminary report). In Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 332-344.

CITED BY 49

	Daniel Jackson , Somesh Jha , Craig A. Damon, Isomorph-free model enumeration: a new method for checking relational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.2, p.302-343, March 1998
	G. Logothetis , K. Schneider, Abstraction from counters: an application on real-time systems, Proceedings of the conference on Design, automation and test in Europe, p.486-493, March 27-30, 2000, Paris, France
	Roberto Giacobazzi , Francesco Ranzato , Francesca Scozzari, Making abstract interpretations complete, Journal of the ACM (JACM), v.47 n.2, p.361-416, March 2000
	Tevfik Bultan, Action Language: a specification language for model checking reactive systems, Proceedings of the 22nd international conference on Software engineering, p.335-344, June 04-11, 2000, Limerick, Ireland
	Roberto Giacobazzi , Francesca Scozzari, A logical model for relational abstract domains, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.5, p.1067-1109, Sept. 1998
	David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States
	Tevfik Bultan , Richard Gerber , William Pugh, Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.4, p.747-789, July 1999
	David A. Schmidt, Structure-preserving binary relations for program abstraction, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
	Doron Bustan , Orna Grumberg, Simulation-based minimization, ACM Transactions on Computational Logic (TOCL), v.4 n.2, p.181-206, April 2003
	Roberto Barbuti , Nicoletta De Francesco , Antonella Santone , Gigiola Vaglini, Logic Based Abstractions of Real-Time Systems, Formal Methods in System Design, v.17 n.3, p.201-220, Dec. 2000
	Henny B. Sipma , Tomás E. Uribe , Zohar Manna, Deductive Model Checking, Formal Methods in System Design, v.15 n.1, p.49-74, July 1999
	Marsha Chechik , Wei Ding, Lightweight reasoning about program correctness, Proceedings of the 2001 conference of the Centre for Advanced Studies on Collaborative research, p.1, November 05-07, 2001, Toronto, Ontario, Canada
	John Hatcliff , Matthew B. Dwyer , Corina S. Păsăreanu , Robby, Foundations of the Bandera abstraction tools, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
	Tevfik Bultan , Richard Gerber , Christopher League, Composite model-checking: verification with type-specific symbolic representations, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.3-50, Jan. 2000
	Patrick Cousot , Radhia Cousot, Temporal abstract interpretation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-25, January 19-21, 2000, Boston, MA, USA
	Marsha Chechik , Benet Devereux , Steve Easterbrook , Arie Gurfinkel, Multi-valued symbolic model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.4, p.371-408, October 2003
	Mila Majster-Cederbaum , Frank Salger, Towards the hierarchical verification of reactive systems, Theoretical Computer Science, v.318 n.3, p.243-296, 8 June 2004
	John Hatcliff , Matthew B. Dwyer , Hongjun Zheng, Slicing Software for Model Construction, Higher-Order and Symbolic Computation, v.13 n.4, p.315-353, Dec. 1, 2000
	Edmund Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav, Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design, v.25 n.2-3, p.105-127, September-November 2004
	Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998
	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
	Marcel kyas , Frank S. de Boer , Willem-paul de Roever, A compositional trace logic for behavioural interface specifications, Nordic Journal of Computing, v.12 n.2, p.116-132, August 2005
	Michael Huth, On finite-state approximants for probabilistic computation tree logic, Theoretical Computer Science, v.346 n.1, p.113-134, 23 November 2005
	María Alpuente , María del Mar Gallardo , Ernesto Pimentel , Alicia Villanueva, A semantic framework for the abstract model checking of tccp programs, Theoretical Computer Science, v.346 n.1, p.58-95, 23 November 2005
	Roberto Barbuti , Nicoletta Francesco , Antonella Santone , Gigliola Vaglini, Reduced Models for Efficient CCS Verification, Formal Methods in System Design, v.26 n.3, p.319-350, May 2005
	María del Mar Gallardo , Jesús Martínez , Pedro Merino , Estefanía Rosales, Using XML to implement abstraction for Model Checking, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain
	Alessandra Di Pierro , Chris Hankin , Herbert Wiklicky, Measuring the confinement of probabilistic systems, Theoretical Computer Science, v.340 n.1, p.3-56, 13 June 2005
	Guillaume Capron, Static analysis of time bounded reactive properties of Boolean symbols, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
	David A. Schmidt, A calculus of logical relations for over- and underapproximating static analyses, Science of Computer Programming, v.64 n.1, p.29-53, January, 2007
	David A. Schmidt, Extracting Program Logics From Abstract Interpretations Defined by Logical Relations, Electronic Notes in Theoretical Computer Science (ENTCS), 173, p.339-356, April, 2007
	Kees van Hee , Olivia Oanea , Alexander Serebrenik , Natalia Sidorova , Marc Voorhoeve, LogLogics: A logic for history-dependent business processes, Science of Computer Programming, v.65 n.1, p.30-40, March, 2007
	Paolo Baldan , Andrea Corradini , Barbara König, A framework for the verification of infinite-state graph transformation systems, Information and Computation, v.206 n.7, p.869-907, July, 2008
	Orna Grumberg , Martin Lange , Martin Leucker , Sharon Shoham, When not losing is better than winning: Abstraction and refinement for the full μ-calculus, Information and Computation, v.205 n.8, p.1130-1148, August, 2007
	Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999
	Patrick Cousot , Radhia Cousot, Refining Model Checking by Abstract Interpretation, Automated Software Engineering, v.6 n.1, p.69-95, January 1999
	Michael R. A. Huth , Radha Jagadeesan , David A. Schmidt, A domain equation for refinement of partial systems, Mathematical Structures in Computer Science, v.14 n.4, p.469-505, August 2004
	Marsha Chechik , Wei Ding, Lightweight Reasoning about Program Correctness, Information Systems Frontiers, v.4 n.4, p.363-377, December 2002
	R. Gentilini , C. Piazza , A. Policriti, From Bisimulation to Simulation: Coarsest Partition Problems, Journal of Automated Reasoning, v.31 n.1, p.73-103, 2003
	Fabricio Fernandes , Jean-Claude Royer, The STSLib Project: Towards a Formal Component Model Based on STS, Electronic Notes in Theoretical Computer Science (ENTCS), 215, p.131-149, June, 2008
	A. Johannes Pretorius , Jarke J. Van Wijk, Visual Analysis of Multivariate State Transition Graphs, IEEE Transactions on Visualization and Computer Graphics, v.12 n.5, p.685-692, September 2006
	Altaf Hussain , Michael Huth, On model checking multiple hybrid views, Theoretical Computer Science, v.404 n.3, p.186-201, September, 2008
	Sunae Seo , Hongseok Yang , Kwangkeun Yi , Taisook Han, Goal-directed weakening of abstract interpretation results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.6, p.39-es, October 2007
	Sharon Shoham , Orna Grumberg, A game-based framework for CTL counterexamples and 3-valued abstraction-refinement, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.1-es, December 2007
	Jens R. Calamé , Natalia Ioustinova , Jaco van de Pol, Automatic Model-Based Generation of Parameterized Test Cases Using Data Abstraction, Electronic Notes in Theoretical Computer Science (ENTCS), 191, p.25-48, October, 2007
	María del Mar Gallardo , Jesús Martínez , Pedro Merino , Ernesto Pimentel, On The Evolution Of Reliability Methods For Critical Software, Journal of Integrated Design & Process Science, v.10 n.4, p.55-67, December 2006
	Sharon Shoham , Orna Grumberg, 3-Valued abstraction: More precision at less cost, Information and Computation, v.206 n.11, p.1313-1333, November, 2008
	José Meseguer , Miguel Palomino , Narciso Martí-Oliet, Equational abstractions, Theoretical Computer Science, v.403 n.2-3, p.239-264, August, 2008
	Alessio Coletta , Roberta Gori , Francesca Levi, Approximating Probabilistic Behaviors of Biological Systems Using Abstract Interpretation, Electronic Notes in Theoretical Computer Science (ENTCS), v.229 n.1, p.165-182, February, 2009
	Adam Antonik , Michael Huth , Kim G. Larsen , Ulrik Nyman , Andrzej Wąsowski, EXPTIME-complete Decision Problems for Modal and Mixed Specifications, Electronic Notes in Theoretical Computer Science (ENTCS), v.242 n.1, p.19-33, July, 2009

INDEX TERMS

Primary Classification:
D. Software
D.2 SOFTWARE ENGINEERING
D.2.4 Software/Program Verification
Subjects: Validation

Additional Classification:
F. Theory of Computation
F.3 LOGICS AND MEANINGS OF PROGRAMS
F.3.1 Specifying and Verifying and Reasoning about Programs
Subjects: Mechanical verification; Logics of programs

General Terms:
Reliability, Theory, Verification

Keywords:
abstract interpretation, formal methods, model checking, mu-calculus, reactive systems

REVIEW

"Richard John Botting : Reviewer"

The “abstract interpretations” in the title are models of “concrete” systems that have fewer states than the original. The abstraction preserves the truth of a requirement expressed as a formula in a modal logic. Checki more...

Collaborative Colleagues:

Dennis Dams: colleagues

Rob Gerth: colleagues

Orna Grumberg: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player