Formal methods for real-time requirements engineering [Elektronische Ressource] / von Georg Rock

Formal Methods for Real-TimeRequirements EngineeringDissertationzur Erlangung des GradesDoktor der Ingenieurwissenschaften (Dr.-Ing.)der Naturwissenschaftlich-Technischen Fakult at Ider Universit at des SaarlandesvonGeorg RockSaarbruc ken, Januar 2004Kolloquium 30. Januar 2004Vorsitz Prof. Dr. Harald Ganzinger, Max-Planck-Institut fur InformatikGutachter Prof. Dr. (PhD) J org Siekmann, Universit at des SaarlandesPriv.-Doz. Dr. Werner Stephan, Universit at des SaarlandesProf. Dr. Wolfgang Reisig, Humboldt-Universit at zu BerlinDekan Prof. Dr.-Ing. Philipp Slusallek, Universit at des SaarlandesContentsAcknowledgements ixAbstract xiKurzzusammenfassung xiiiExtended Abstract xvZusammenfassung xvii1. Introduction 12. Real-Time 72.1 Real-Time . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.2 Speci cation of Real-Time . . . . . . . . . . . . . . . . . . . . . . . 82.2.1 Temporal Logic as Basis . . . . . . . . . . . . . . . . . . . . 92.2.2 Expressing Timing Constraints . . . . . . . . . . . . . . . . 102.2.3 Real-Time Logics . . . . . . . . . . . . . . . . . . . . . . . . 122.3 Models of Time . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132.3.1 Basics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142.3.2 Relations between Basic Time Elements . . . . . . . . . . . 142.3.3 Time Model Used . . . . . . . . . . . . . . . . . . . . . . . . 163. Gasburner Scenario 193.1 An Abstract Version . . . . . . . . . .