Action Refinement as an Implementation Relation

Arend Rensink; M. Dauchet; R. Gorrieri

doi:10.1007/BFb0030640

Action Refinement as an Implementation Relation

Arend Rensink, M. Dauchet (Editor), R. Gorrieri

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

13 Citations (Scopus)

126 Downloads (Pure)

Abstract

We propose a theory of process refinement which relates behavioural descriptions belonging to conceptually different abstraction levels, through a so-called vertical implementation relation. The theory is based on action refinement, which permits to relate abstract actions of the implementation to concrete computations of the implementation; it is developed in the standard interleaving approach. A number of proof rules is shown to be sound for the particular vertical implementation relation (based on observation congruence) we study in this paper. We give an illustrative example.

Original language	English
Title of host publication	TAPSOFT '97: Theory and Practice of Software Development
Subtitle of host publication	7th International Joint Conference CAAP/FASE Lille, France, April 14–18, 1997. Proceedings
Editors	Michel Bidoit, Max Dauchet
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	772-786
Number of pages	15
ISBN (Electronic)	978-3-540-68517-3
ISBN (Print)	978-3-540-62781-4
DOIs	https://doi.org/10.1007/BFb0030640
Publication status	Published - 1997
Event	7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, TAPSOFT 1997 - Lille, France Duration: 14 Apr 1997 → 18 Apr 1997 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1214
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, TAPSOFT 1997
Abbreviated title	TAPSOFT
Country/Territory	France
City	Lille
Period	14/04/97 → 18/04/97

Keywords

Transition system
Operational semantics
Abstraction level
Abstract action
Refinement function

Access to Document

10.1007/BFb0030640

Rensink1997actionAccepted author version, 272 KB

Cite this

Rensink, A., Dauchet, M. (Ed.), & Gorrieri, R. (1997). Action Refinement as an Implementation Relation. In M. Bidoit, & M. Dauchet (Eds.), TAPSOFT '97: Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE Lille, France, April 14–18, 1997. Proceedings (pp. 772-786). (Lecture Notes in Computer Science; Vol. 1214). Springer. https://doi.org/10.1007/BFb0030640

Rensink, Arend ; Dauchet, M. (Editor) ; Gorrieri, R. / Action Refinement as an Implementation Relation. TAPSOFT '97: Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE Lille, France, April 14–18, 1997. Proceedings. editor / Michel Bidoit ; Max Dauchet. Berlin, Heidelberg : Springer, 1997. pp. 772-786 (Lecture Notes in Computer Science).

@inproceedings{58d37289ba3643dca718440c158b9f12,

title = "Action Refinement as an Implementation Relation",

abstract = "We propose a theory of process refinement which relates behavioural descriptions belonging to conceptually different abstraction levels, through a so-called vertical implementation relation. The theory is based on action refinement, which permits to relate abstract actions of the implementation to concrete computations of the implementation; it is developed in the standard interleaving approach. A number of proof rules is shown to be sound for the particular vertical implementation relation (based on observation congruence) we study in this paper. We give an illustrative example.",

keywords = "Transition system, Operational semantics, Abstraction level, Abstract action, Refinement function",

author = "Arend Rensink and M. Dauchet and R. Gorrieri",

year = "1997",

doi = "10.1007/BFb0030640",

language = "English",

isbn = "978-3-540-62781-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "772--786",

editor = "Michel Bidoit and Max Dauchet",

booktitle = "TAPSOFT '97: Theory and Practice of Software Development",

address = "Germany",

note = "7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, TAPSOFT 1997, TAPSOFT ; Conference date: 14-04-1997 Through 18-04-1997",

}

Rensink, A, Dauchet, M (ed.) & Gorrieri, R 1997, Action Refinement as an Implementation Relation. in M Bidoit & M Dauchet (eds), TAPSOFT '97: Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE Lille, France, April 14–18, 1997. Proceedings. Lecture Notes in Computer Science, vol. 1214, Springer, Berlin, Heidelberg, pp. 772-786, 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, TAPSOFT 1997, Lille, France, 14/04/97. https://doi.org/10.1007/BFb0030640

Action Refinement as an Implementation Relation. / Rensink, Arend; Dauchet, M. (Editor); Gorrieri, R.
TAPSOFT '97: Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE Lille, France, April 14–18, 1997. Proceedings. ed. / Michel Bidoit; Max Dauchet. Berlin, Heidelberg: Springer, 1997. p. 772-786 (Lecture Notes in Computer Science; Vol. 1214).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Action Refinement as an Implementation Relation

AU - Rensink, Arend

AU - Gorrieri, R.

A2 - Dauchet, M.

A2 - Bidoit, Michel

A2 - Dauchet, Max

N1 - Conference code: 7

PY - 1997

Y1 - 1997

N2 - We propose a theory of process refinement which relates behavioural descriptions belonging to conceptually different abstraction levels, through a so-called vertical implementation relation. The theory is based on action refinement, which permits to relate abstract actions of the implementation to concrete computations of the implementation; it is developed in the standard interleaving approach. A number of proof rules is shown to be sound for the particular vertical implementation relation (based on observation congruence) we study in this paper. We give an illustrative example.

AB - We propose a theory of process refinement which relates behavioural descriptions belonging to conceptually different abstraction levels, through a so-called vertical implementation relation. The theory is based on action refinement, which permits to relate abstract actions of the implementation to concrete computations of the implementation; it is developed in the standard interleaving approach. A number of proof rules is shown to be sound for the particular vertical implementation relation (based on observation congruence) we study in this paper. We give an illustrative example.

KW - Transition system

KW - Operational semantics

KW - Abstraction level

KW - Abstract action

KW - Refinement function

U2 - 10.1007/BFb0030640

DO - 10.1007/BFb0030640

M3 - Conference contribution

SN - 978-3-540-62781-4

T3 - Lecture Notes in Computer Science

SP - 772

EP - 786

BT - TAPSOFT '97: Theory and Practice of Software Development

PB - Springer

CY - Berlin, Heidelberg

T2 - 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, TAPSOFT 1997

Y2 - 14 April 1997 through 18 April 1997

ER -

Rensink A, Dauchet M, (ed.), Gorrieri R. Action Refinement as an Implementation Relation. In Bidoit M, Dauchet M, editors, TAPSOFT '97: Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE Lille, France, April 14–18, 1997. Proceedings. Berlin, Heidelberg: Springer. 1997. p. 772-786. (Lecture Notes in Computer Science). doi: 10.1007/BFb0030640

Action Refinement as an Implementation Relation

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this