Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Refinement preserving approximations for the design and verification of heterogeneous systems

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Embedded systems are electronic devices that function in the context of a real environment, by sensing and reacting to a set of stimuli. Because of their close interaction with the environment, and to simplify their design, different parts of an embedded system are best described using different notations and different techniques. In this case, we say that the system is heterogeneous. We informally refer to the notation and the rules that are used to specify and verify the elements of heterogeneous systems and their collective behavior as a model of computation. In this paper, we consider different classes of relationships between models of computation and discuss their preservation properties with respect to the model's refinement relation and composition operator. In particular, we focus on abstraction and refinement relationships in the form of abstract interpretations and introduce the notion of conservative approximation. We show that, unlike abstract interpretations, conservative approximations preserve refinement verification results from an abstract to a concrete model while avoiding false positives. We also characterize the relationship between abstract interpretations and conservative approximations, and derive necessary and sufficient conditions to obtain a conservative approximation from a pair of abstract interpretations. In addition, we use the inverse of a conservative approximation to identify components that can be used indifferently in several models, thus enabling reuse across models of computation. The concepts described in this paper are illustrated with examples from continuous time and discrete time models of computation.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Alur R, Itai A, Kurshan R, Yannakakis M (1995) Timing verification by successive approximation. Inf Comput 118(1):142–157

    Google Scholar 

  2. Balarin F, Lavagno L, Passerone C, Sangiovanni-Vincentelli A, Watanabe Y, Yang G (2002) Concurrent execution semantics and sequential simulation algorithms for the metropolis meta-model. In: Proceedings of the tenth international symposium on hardware/software codesign. Estes Park, CO, May 2002

  3. Burch JR (1992) Trace algebra for automatic verification of real-time concurrent systems. PhD thesis, School of Computer Science, Carnegie Mellon University

  4. Burch JR, Passerone R, Sangiovanni-Vincentelli AL (2001) Overcoming heterophobia: modeling concurrency in heterogeneous systems. In: Koutny M, Yakovlev A (eds) Application of concurrency to system design

  5. Burch JR, Passerone R, Sangiovanni-Vincentelli AL (2001) Using multiple levels of abstractions in embedded software design. In: Henzinger and Kirsch [14], pp 324–343

  6. Burch JR, Passerone R, Sangiovanni-Vincentelli AL (2002) Modeling techniques in design-by-refinement methodologies. In: Proceedings of the sixth biennial world conference on integrated design and process technology

  7. Clarke EM, Grumberg O, Peled D (1999) Model checking, 2nd edn. The MIT Press, Cambridge, MA

  8. Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference record of the fourth annual ACM SIGPLAN-SIGACT symposium on principles of programming languages. Los Angeles, California. ACM Press, New York, NY, pp 238–252

  9. Cousot P, Cousot R (1992) Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In: Bruynooghe M, Wirsing M (eds) Proceedings of the international workshop programming language implementation and logic programming, PLILP’92, Leuven, Belgium, Lecture notes in computer science, volume 631. Springer-Verlag, Berlin, Germany, pp 269–295

  10. Das S, Dill DL (2001) Successive approximation of abstract transition relations. In: Proceedings of the sixteenth annual IEEE symposium on logic in computer science. Boston, MA

  11. Dill DL (1989) Trace theory for automatic hierarchical verification of speed-independent circuits. ACM Distinguished Dissertations. MIT Press

  12. Erné M, Koslowski J, Melton A, Strecker GE (1993) A primer on galois connections. In: Papers on general topology and applications, volume 704 of Ann. New Yosk Acad. Sci. Madison, WI, pp 103–125

  13. Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: Computer-aided verification, proceedings of the 1997 workshop, volume 1254 of Lectures notes in computer science

  14. Henzinger TA, Kirsch CM (eds) (2001) Embedded software, volume 2211 of Lecture notes in computer science. Springer-Verlag

  15. Kurshan RP, McMillan KL (1991) Analysis of digital circuits through symbolic reduction. IEEE Trans Comput-Aided Design Integr Circuits 10(11):1356–1371

    Article  Google Scholar 

  16. Kurshan RP (1995) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press

  17. Lee EA, Sangiovanni-Vincentelli AL (1998) A framework for comparing models of computation. IEEE Trans Comput-Aided Design Integr Circuits 17(12):1217–1229

    Article  Google Scholar 

  18. Lee EA (2003) Overview of the Ptolemy project. Technical memorandum UCB/ERL M03/25. University of California, Berkeley

  19. Lee EA, Xiong Y (2001) System-level types for component-based design. In: Henzinger and Kirsch [14]

  20. Loiseaux C, Graf S, Sifakis J, Bouajjani A, Bensalem S (1995) Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst Des 6:1–35

    Google Scholar 

  21. Moriconi M, Qian X, Riemenschneider RA (1995) Correct architecture refinement. IEEE Trans Softw Eng 21(4):356–372

    Article  Google Scholar 

  22. Negulescu R (1998) Process spaces and the formal verification of asynchronous circuits. PhD thesis, University of Waterloo, Canada

  23. Pasareanu C, Pelánek R, Visser W (2005) Concrete model checking with abstract matching and refinement. In: Proceedings of the 17th international conference on computer-aided verification, volume 3576 of Lecture notes in computer science. Springer-Verlag

  24. Passerone R (2004) Semantic foundations for heterogeneous systems. PhD thesis, Department of EECS, University of California at Berkeley, 2004

  25. Sassone V, Nielsen M, Winskel G (1996) Models for concurrency: towards a classification. Theor Comput Sci 170:297–348

    MATH  MathSciNet  Google Scholar 

  26. Sutherland WA (1975) Introduction to metric and topological spaces. Oxford University Press, London, UK

    MATH  Google Scholar 

Download references

Author information

Author notes

  1. Roberto Passerone

    Present address: Department of Information and Communication Technology, University of Trento, via Sommarive 14, 38050, Povo, TN, Italy

Authors and Affiliations

  1. Cadence Design Systems, 1995 University Ave Suite 460, Berkeley, CA, 94709, USA

    Roberto Passerone

  2. Synopsys, Inc., 2025 NW Cornelius Pass Rd., Hillsboro, 97124, USA

    Jerry R. Burch

  3. Department of EECS, University of California, Berkeley, Berkeley CA, 94720, USA

    Alberto L. Sangiovanni-Vincentelli

Authors
  1. Roberto Passerone
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jerry R. Burch
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto L. Sangiovanni-Vincentelli
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Passerone, R., Burch, J.R. & Sangiovanni-Vincentelli, A.L. Refinement preserving approximations for the design and verification of heterogeneous systems. Form Methods Syst Des 31, 1–33 (2007). https://doi.org/10.1007/s10703-006-0024-z

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-006-0024-z

Keywords

Search

Navigation