High level transition systems of CSP specifications and their application in automated testing [Elektronische Ressource] / von Markus Dahlweid und Uwe Schulze
High Level Transition Systems of CSPSpeci cations and their Application inAutomated Testingvon Markus Dahlweidund Uwe SchulzeDissertationzur Erlangung des Grades eines Doktors derIngenieurwissenschaften— Dr.–Ing. —Vorgelegt im Fachbereich 3 (Mathematik & Informatik)der Universit at Bremenim Oktober 2003Datum des Promotionskolloquiums: 02. Februar 2004Gutachter: Prof. Dr. Jan Peleska (Universitat Bremen)Prof. Dr. Hans-J org Kreowski (Universit at Bremen)iiiAbstractState of the art quality assurance for safety critical software systems requiresformal methods for veri cation and testing. The context of this thesis is the eldof speci cation based testing of embedded reactive real-time systems. One of thedrawbacks using formal methods to model large systems is the state explosionof transition systems generated from formal speci cations. In this PhD-thesisthe authors present an approach to reduce the problem of state explosions usinga representation of the transition system of a CSP speci cation, that does notrequire the calculation of the complete state space.The new representation consists of two parts: high level transition graphs tomodel sequential processes containing only low-level CSP operators and synchro-nisation terms that represent the high-level communication structure of sequen-tialcomponentsexpressedusinghighleveltransitiongraphs.