TY - GEN
T1 - Testing and refinement for nondeterministic and probabilistic processes
AU - Jonsson, Bengt
AU - Ho-Stuart, Chris
AU - Yi, Wang
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1994.
PY - 1994
Y1 - 1994
N2 - Transition systems are a basic semantic model for formal description, specification, and analysis of concurrent and distributed systems. In order to describe and analyze aspects of reliability, such as the likelihood of trace and failure, this model has been extended in various ways to handle probabilistic behavior. To use these models for specification and stepwise development of systems, it is important to develop appropriate refinement preorders. In the paper, we develop refinement preorders based on a framework of testing for a model that represents both nondeterministic and probabilistic choices as independent concepts [YL92]. Our main contribution is a notion of reward testing, and a denotational characterization of a testing preorder, which corresponds to a natural probabilistic extension of the trace model [Hoa85].
AB - Transition systems are a basic semantic model for formal description, specification, and analysis of concurrent and distributed systems. In order to describe and analyze aspects of reliability, such as the likelihood of trace and failure, this model has been extended in various ways to handle probabilistic behavior. To use these models for specification and stepwise development of systems, it is important to develop appropriate refinement preorders. In the paper, we develop refinement preorders based on a framework of testing for a model that represents both nondeterministic and probabilistic choices as independent concepts [YL92]. Our main contribution is a notion of reward testing, and a denotational characterization of a testing preorder, which corresponds to a natural probabilistic extension of the trace model [Hoa85].
UR - https://www.scopus.com/pages/publications/0009616739
U2 - 10.1007/3-540-58468-4_176
DO - 10.1007/3-540-58468-4_176
M3 - 会议稿件
AN - SCOPUS:0009616739
SN - 9783540584681
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 418
EP - 430
BT - Formal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings
A2 - Langmaack, Hans
A2 - de Roever, Willem-Paul
A2 - Vytopil, Jan
A2 - Vytopil, Jan
PB - Springer Verlag
T2 - 3rd International Symposium on Formal Techniques in Real Time and Fault Tolerance Organized Jointly with Working Group Provably Correct Systems, ProCoS 1994
Y2 - 19 September 1994 through 23 September 1994
ER -