Approach:

This report treats methods for simplifying (and abstracting) the physical environment model prior to composition with the controller.  We show how models of the environment as an open system, expressed as hybrid transition systems (HTS), can be step-wise transformed to hybrid automata (HA) or mode-automata given certain assumptions on the inputs to the model. We distinguish between controller actions and unmodelled physical variables (disturbances). Four types of restrictions on input signals are considered:

(1) piece-wise constant with finite range of values
        a. constant throughout the run
        b. changing at equidistance time points
        c. changing at times when borders of partitions in the state space are crossed
(2) piece-wise constant slope

For each assumption, a number of modes with simpler dynamics replace a mode with more complex dynamics.

Achieved Results: The air control case study, physically modelled in year 1 of the project, is used to illustrate

• Transformations resulting from different restrictions on input signals:
• Applying restrictions of type (1), (1)a and (1)b to suitable inputs, the model is transformed to a mode-automaton which is in turn compilable to a Lustre program, composed with the controller, and further compiled to input format of theorem provers (PVS or NP-Tools).
• Applying restrictions of type (1)a and (2) to suitable inputs, the model is transformed to a hybrid automaton where variables evolve linearly in time or in a linear fashion wrt other variables. This model is intended to be used for algorithmic verification using the Polka tool later in the project.
• Applying restrictions of type (1) and (1)a only, is illustrated to give a higher number of modes in the transformed model, due to lack of continuity in the control signal from the (not apriori fixed) controller. Restriction to (1)c type of signals does not apply to the case study.
• Refinements of the requirements specifications, showing:
• How can sufficient conditions for proving a property be derived based on restrictions above.
• How can formal and informal reasoning in the form of theorem proving and mathematical analysis be combined to prove safety and timeliness properties. Proofs for some sufficient conditions performed in NP-Tools are thus placed in a context.

• S. Nadjm-Tehrani

Integration of Analog and Discrete Synchronous Design
Draft report, Submitted for publication. 1998.