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.

Refinement Preserving Approximations for the Design and Verification of Heterogeneous Systems / Passerone, Roberto; J. R., Burch; A. L., Sangiovanni Vincentelli. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - STAMPA. - 31:1(2007), pp. 1-33.

Refinement Preserving Approximations for the Design and Verification of Heterogeneous Systems

Passerone, Roberto;
2007-01-01

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.
2007
1
Passerone, Roberto; J. R., Burch; A. L., Sangiovanni Vincentelli
Refinement Preserving Approximations for the Design and Verification of Heterogeneous Systems / Passerone, Roberto; J. R., Burch; A. L., Sangiovanni Vincentelli. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - STAMPA. - 31:1(2007), pp. 1-33.
File in questo prodotto:
File Dimensione Formato  
PasseroneBurchASV07FMSD.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 500 kB
Formato Adobe PDF
500 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/66232
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 8
social impact