Refinement preserving approximations for the design and verification of heterogeneous systems.

*(English)*Zbl 1118.68498Summary: 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.

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.

##### MSC:

68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |

##### Keywords:

Refinement; Preserving; Approximation; Abstraction; Verification; Heterogeneous; Reuse; Polymorphism; Model of computation; Galois connection; Abstract interpretation; Conservative approximation; Continuous time; Discrete time; Concretization
PDF
BibTeX
XML
Cite

\textit{R. Passerone} et al., Form. Methods Syst. Des. 31, No. 1, 1--33 (2007; Zbl 1118.68498)

Full Text:
DOI

##### References:

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

[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 · Zbl 1050.68521 |

[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 · Zbl 0809.06006 |

[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 · Zbl 05448666 · doi:10.1109/43.97615 |

[16] | Kurshan RP (1995) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press · Zbl 0822.68116 |

[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 · Zbl 05448730 · doi:10.1109/43.736561 |

[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] · Zbl 1050.68528 |

[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 · Zbl 0829.68053 |

[21] | Moriconi M, Qian X, Riemenschneider RA (1995) Correct architecture refinement. IEEE Trans Softw Eng 21(4):356–372 · Zbl 05113677 · doi:10.1109/32.385972 |

[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 · Zbl 0874.68120 |

[26] | Sutherland WA (1975) Introduction to metric and topological spaces. Oxford University Press, London, UK · Zbl 0304.54002 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.