https://ir.unisa.ac.za/handle/10500/23892 Fri, 19 Jun 2026 20:23:50 GMT 2026-06-19T20:23:50Z https://ir.unisa.ac.za/handle/10500/25449 WOFACS '96: Workshop on formal and applied Computer Science Brink, C Wed, 01 Jan 1997 00:00:00 GMT https://ir.unisa.ac.za/handle/10500/25449 1997-01-01T00:00:00Z https://ir.unisa.ac.za/handle/10500/24260 Verification of finite state systems with temporal logic model checking Schlingloff, B These tutorial notes contain an introduction to the logical theory and computational aspects of computer aided verification of finite state reactive systems with linear and branching temporal logic model checking. As a general recipe, computer science applications and algorithms are derived from logical notions and proofs. First, the expressivity of various temporal logics is compared to first and second order logic, and to w-automata and formal languages. Then, temporal safety and liveness properties are reviewed. From the completeness proof for natural and tree models, local and global decision procedures are developed. These in turn give rise to the corresponding model checking procedures. Various modelling techniques for reactive systems are presented. Finally, symbolic techniques for global model checking with binary decision diagrams, and partial order techniques for local model checking with stubborn sets are discussed. Wed, 01 Jan 1997 00:00:00 GMT https://ir.unisa.ac.za/handle/10500/24260 1997-01-01T00:00:00Z https://ir.unisa.ac.za/handle/10500/24259 Test automation of safety-critical reactive systems Peleska, J; Siegel, M This article focuses on test automation for safety-critical reactive systems. In the first part of the paper we introduce a methodology for specification, design and verification of fault-tolerant systems allowing to combine different methods in a systematic and consistent way, provided that these methods are compositional. The methodology indicates how to "switch" between formal verification and testing during the construction of (possibly large) reactive systems. We introduce the basic notions of testing as far as relevant in the context of reactive systems and relate them to the verification methodology. Part II formally describes our test automation method which is based on Hoare's CSP and takes Hennessy's testing theory as a starting point. It is indicated how this specific method fits into the general approach described in Part I. We introduce CSP test drivers which are trustworthy in the sense that they "approximate" refinement proofs, converging to a full proof with the increasing (possibly infinite) number of tests successfully executed. These drivers have been implemented in the VVT-RT (Verification, Validation and Test for Reactive Real-Time Systems) tool developed at Bremen University in cooperation with the University of Kiel, JP Software-Consulting and ELPRO LET GmbH. The presentation of this article is based on the lectures given by the first author during the WOFACS '96 workshop at the University of Cape Town. Wed, 01 Jan 1997 00:00:00 GMT https://ir.unisa.ac.za/handle/10500/24259 1997-01-01T00:00:00Z https://ir.unisa.ac.za/handle/10500/24258 Application-oriented program semantics McIver, AK; Morgan, C; Sanders, JW This paper abridges lecture notes from WOFACS 96. It provides semantic models for a variety of programming and development formalisms, showing how different models for the same formalism are related by Galois connections. The formalisms are: the language of guarded commands and its refinement calculus; communicating sequential processes; and probabilistic imperative code. The semantic models include: binary relations; predicate transformers; traces; failures; and distributions. In each case, denotations of code are characterised, in the more general specification space, by the healthiness conditions they satisfy. Models are evaulated for their elegance, expressive power and calculational facility. Expanded notes containing proofs, an extra chapter on data refinement and exercises for each chapter, are available from the au­thors. Wed, 01 Jan 1997 00:00:00 GMT https://ir.unisa.ac.za/handle/10500/24258 1997-01-01T00:00:00Z