In this paper a generic framework inspired by [LX90] is presented for the validation of reactive systems embedded in a test environment, or isolated from their operational environment, thereby inducing a natural classification of validation strategies in different scenarios. We show that verification strategies and falsification strategies are complementary notions (but not necessarily equally strong), and how the choice of strategy for assessing the correctness of systems in different scenarios affects the outcome of the validation process. The significance of this paper lies in the provision of systematic principles to perform validation in context, and it gives a theoretical explanation of validation strategies that have already been applied informally in practice. The theory in this paper provides a guide for performing correctness assessment of systems in context, and shows that the correctness of systems in such cases can be approximated in the sense that the risk of considering an incorrect system correct can be reduced systematically.


approximation environment falsification process property property transformer validation scenario validation strategy verification 


  1. [BS90]
    Julian Bradfield and Colin Stirling. Verifying temporal properties of processes. In J. C. M. Baeten and J. W. Klop, editors, Concur ’80, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990.Google Scholar
  2. [BTV91]
    Ed Brinksma, Jan Tretmans, and Louis Verhaard. A framework for test selection. In B. Jonsson, J. Parrow, and B. Pehrson, editors, Protocol Specification, Testing, and Verification, XI, pages 233–248. North-Holland Publishing Company, 1991.Google Scholar
  3. [ISO89]
    ISO. Information processing systems — open systems interconnection — LOTOS — a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807, ISO, Geneva, February 1989.Google Scholar
  4. [ISO91]
    ISO. Information technology, open systems interconnection, conformance testing methodology and framework. Technical Report 9646, ISO, Geneva, 1991.Google Scholar
  5. [LX90]
    Kim Guldstrand Larsen and Liu Xinxin. Compositionality through an operational semantics of contexts. In M. S. Paterson, editor, Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 526–539. Springer-Verlag, 1990.Google Scholar
  6. [Mi180]
    R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.Google Scholar
  7. [Pop63]
    K.R. Popper. Conjectures and Refutations. Routledge and Kegan Paul, London, 1963.Google Scholar
  8. [PYD94]
    A. Petrenko, N. Yevtushenko, and R. Dssouli. Testing strategies for communicating FSMs. In T. Mizuno et al., editor, International Workshop on Protocol Test Systems VII pages 181–196, 1994. Participants proceedings.Google Scholar
  9. [Tre92]
    Jan Tretmans. A Formal Approach to Conformance Testing. PhD thesis, University of Twente, December 1992.Google Scholar
  10. [TV92]
    Jan Tretmans and Louis Verhaard. A queue model relating synchronous and asynchronous communication. In Protocol Specification, Testing, and Verification, XII. North-Holland Publishing Company, 1992.Google Scholar
  11. [Vic89]
    Steven Vickers. Topology via Logic. Cambridge University Press, 1989.zbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • Lex Heerink
    • 1
  • Ed Brinksma
    • 1
  1. 1.Tele-Informatics and Open Systems groupUniversity of TwenteEnschedeThe Netherlands

Personalised recommendations