In this paper we propose a model for the specification of non-deterministic systems based on a functional approach. The behaviour of a System is specified by means of a predicate, functional specification in the sequel, which characterize a set of sequence processing monotonie functions. We introduce a set of combination on sequence processing functions and on functional specifications. Such combinators together give rise to a Functional Algebra (FA) and then allow for sys-tematically build specifications in a compositional way. FA is takes as the natural denotational model for a simple algebra of processes with input/output actions (PA). PA operators are STOP, input/output-prefix, which is a functional variant of action-prefix, and choice. We show that, under proper conditions, FA is fully abstract w.r.t Test-ing Equivalence when actions are interpreted as input/output pairs. Moreover, we show how full abstraction can still be guaranteed even for the whole PA provided the notion of experimenter be modified in order to take into account the conceptual separation between input events and output events peculiar of the functional approach.
A functional approch to testing equivalence
Latella D;Massink M;Pedreschi D
1994
Abstract
In this paper we propose a model for the specification of non-deterministic systems based on a functional approach. The behaviour of a System is specified by means of a predicate, functional specification in the sequel, which characterize a set of sequence processing monotonie functions. We introduce a set of combination on sequence processing functions and on functional specifications. Such combinators together give rise to a Functional Algebra (FA) and then allow for sys-tematically build specifications in a compositional way. FA is takes as the natural denotational model for a simple algebra of processes with input/output actions (PA). PA operators are STOP, input/output-prefix, which is a functional variant of action-prefix, and choice. We show that, under proper conditions, FA is fully abstract w.r.t Test-ing Equivalence when actions are interpreted as input/output pairs. Moreover, we show how full abstraction can still be guaranteed even for the whole PA provided the notion of experimenter be modified in order to take into account the conceptual separation between input events and output events peculiar of the functional approach.File | Dimensione | Formato | |
---|---|---|---|
prod_409655-doc_144068.pdf
accesso aperto
Descrizione: A functional approch to testing equivalence
Dimensione
4.77 MB
Formato
Adobe PDF
|
4.77 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.