High Level Transition Systems of CSP Specifications and their Application in Automated Testing

Abstract

State of the art quality assurance for safety critical software systems requires formal methods for verification and testing. The context of this thesis is the field of specification based testing of embedded reactive real-time systems. The authors present an approach to reduce the problem of state explosions using a representation of the transition system of a CSP specification, that does not require the calculation of the complete state space.The new representation consists of two parts: High-Level transition graphs (HLTG) to model sequential processes containing only low-level CSP operators and synchronisation terms that represent the high-level communication structure of sequential components expressed using high-level transition graphs. HLTG are an extension of conventional transition systems, which contain events, conditions and assignments of CSP specifications at the transitions, containing parameters and parametrised expressions. The value of a parameter is bound through assignments at transitions, which are created for the CSP operators prefixing and process references. A node in a HLTG can represent multiple states of the complete state space. The interpretation of a HLTG requires the evaluation of the conditions, events and assignments of a transition to perform a state change.Real-time testing requires an upper bound of time required for the calculation of the initial actions and refusals of a location. This can be achieved by using normalised transition systems. Different stages of the normalisation of HLTG and synchronisation terms have been developed. To enable real-time testing with unnormalised graphs, an on-the-fly normalisation is introduced. For those cases, where test evaluation needs not to be performed in real-time, a new test algorithm for a delayed test evaluation is suggested, which can be used for testing purposes based on any type of transition systems, even unnormalised systems.