Techniques for Property Preservation in the Development of Real-Time Systems
This thesis examines the problem of formal modeling of real-time requirements and the problem of property preservation in the context of model-based computer aided development of reactive real-time systems. Demanded system behavior is modeled using a denotational framework which is able to capture and interrelate time and functional requirements. Using this framework time requirements can be formulated, analyzed resp. consistency and completeness, and related to component architectures. In order to ensure property preservation, a model-based transformation method is developed. For the transitions from application logic to task architecture and from task architecture to deployed system synthesis procedures are presented and their correctness is formally proved.