Abstract
By a hybrid system we mean a discrete controller in interaction with a physical environment. This paper discusses methodologies for incorporating physically grounded models in representations of hybrid systems. To this end, we study a driver support system, an example which includes unmodelled inputs. We consider models at different levels of abstraction. First, we show that discrete models of the environment can be obtained from the continuous models without losing relevant information. We do this using an analysis of the continuous state space. Dynamic Transition Systems (DTS) are used for the modular modelling at this level of abstraction. Next, we consider models using Hybrid Transition Systems (HTS). This can be seen as a modular version of timed transition systems allowing both differential and algebraic equations in each mode. Finally, we comment on expressivity requirements on hybrid formalisms for modelling realistic physical systems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and L. Lamport. An Old-Fashioned Recipe for Real-Time. In de Bakker et al. [7], pages 1–27.
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for Real-Time Systems. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 414–425. Computer Society Press, 1990.
R. Alur, T.A. Henzinger, and P.H. Ho. Automatic Symbolic Verification of Embedded Systems. In Proc. of Real Time Systems Symposium. Computer Society Press, 1993.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proc. IEEE Conf. on Logic in Computer Science, pages 428–439. Computer Society Press, 1990.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986. An early version of the paper appeared at the 10th ACM symposium on principles of programming languages, 1983.
E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another Look at LTL Model Checking. In Proc. 6th Int. Conf. on Computer Aided Verification (CAV'94). Springer Verlag, 1994.
J.W. de Bakker, C. Huizing, W.P. de Roever, and G.Rozenberg, editors. Proc. REX workshop 1991. Springer Verlag, LNCS 600, 1992.
E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative Temporal Reasoning. Real-Time Systems, 4:331–352, 1992. An early version of the paper appeared at the workshop on automatic verification methods for finite state systems, Grenoble, 1989.
R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors. Proc. Workshop on Theory of Hybrid Systems, October 1992, LNCS 736, Lyngby, Denmark, 1993. Springer Verlag.
E. Harel, O. Lichtenstein, and A. Pnueli. Explicit Clock Temporal Logic. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 402–413. Computer Society Press, 1990.
T.A. Henzinger, Z. Manna, and A. Pnueli. Temporal Proof Methodologies for Real-Time Systems. In 18th ACM Symp. on Principles of Programming Languages, pages 353–366, 1991.
T.A Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-time Systems. In proceedings of IEEE Symposium on Logic in Computer Science, pages 394–406. Computer Society Press, 1992.
R. Kaivola. Compositional Model Checking for Linear-Time Temporal Logic. In Proc. 4th int. workshop on Computer Aided Verification, pages 248–259. Springer Verlag, 1992.
D.C. Karnopp, R.C. Rosenberg, and D. Margolis. System dynamics — A unified approach (2nd edition). John Wiley & Sons, New York, 1990.
Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration Graphs: A Class of Decidable Hybrid Systems. In Grossman et al.[9], pages 179–208.
D. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, School of Computer Science, Carnegie Mellon University, July 1993. CMU-CS-93-178.
N. Lynch and F. Vaandrager. Forward and Backward Simulations, Part I: Untimed Systems. Technical Report MIT/LCS/TM-486, Laboratory for Computer science, MIT, May 1993.
N. Lynch and F. Vaandrager. Forward and Backward Simulations, Part II: Timing-based Systems. Technical Report MIT/LCS/TM-487, Laboratory for Computer science, MIT, May 1993.
O. Maler, Z. Manna, and A. Pnueli. From Timed to Hybrid Systems. In de Bakker et al. [7], pages 447–484.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems — volume I. Springer Verlag, 1991.
Z. Manna and A. Pnueli. Verifying Hybrid Systems. In Grossman et al.[9], pages 4–35.
K. Marzullo, F. B. Schneider, and N. Budhiraja. Derivation of Sequential, Real-time, Process Control Programs. In A.M. van Tilborg and G.M. Koob, editors, Foundations of Real-Time Computing, Volume I: Formal Specifications and Methods, pages 39–54. Kluwer Academic Publishers, 1991.
M. Morin, S. Nadjm-Tehrani, P. österling, and E. Sandewall. Real-Time Hierarchical Control. IEEE Software, 9(5):51–57, September 1992.
S. Nadjm-Tehrani. Reactive Systems in Physical Environments: Compositional Modelling and Framework for Verification. PhD thesis, Dept. of Computer and Information Science, Linköping University, March 1994. Dissertation No. 338.
X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An Approach to Description and Analysis of Hybrid Systems. In Grossman et al. [9], pages 149–178.
J. S. Ostroff. Temporal Logic for Real-Time Systems. Research Studies Press Ltd., Somerset, 1989.
J. S. Ostroff. Deciding Properties of Timed Transition Models. IEEE Transactions on Parallel and Distributed Systems, 1(2):170–183, April 1990.
H. M. Paynter. Analysis and design of engineering systems. MIT Press, Cambridge, Mass., 1961.
A. P. Ravn and H. Rischel. Requirements Capture for Embedded Real-Time Systems. In IMACS-IFAC Symposium: Modelling and Control of Technological Systems. IMACS, May 1991.
E. Sandewall. Combining Logic and Differential Equations for Describing Realworld Systems. In Proceedings of the Eleventh International Joint Conference on Artificial Intelligence (IJCAI'89), Detroit, pages 412–420. Morgan. Kaufman, 1989.
E.D. Sontag. Nonlinear regulation: the piecewise linear approach. IEEE Trans. on Automatic Control, 26(2), April 1981.
J.A. Stiver and P.J. Antsaklis. Modeling and Analysis of Hybrid Systems. In Proc. of the 31st IEEE Conf. on Decision and Control (CDC '92), pages 3748–3751, Tucson, 1992.
J.E. Strömberg and S. Nadjm-Tehrani. On Discrete and Hybrid Representation of Hybrid Systems. In Proceedings of the SCS International Conference on Modeling and Simulation (ESM '94), pages 1085–1089, Barcelona, June 1994.
J.E. Strömberg, J. Top, and U. Söderman. Variable causality in bond graphs caused by discrete effects. In Proc. First Int. Conf. on Bond Graph Modeling (ICBGM '93), number 2 in SCS Simulation Series, volume 25, pages 115–119, San Diego, 1993.
F. Wang, A.K. Mok, and E. A. Emerson. Symbolic Model Checking for Distributed Real-Time Systems. In J.C.P. Woodcock and P.G. Larsen, editors, Proceedings of the first Int. Symposium of Formal Methods Europe, FME'93: Industrial-Strength Formal Methods, pages 632–651. Springer Verlag, 1993.
D. S. Weld and J. de Kleer, editors. Readings in Qualitative Reasoning about Physical Systems. Morgan Kaufman, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nadjm-Tehrani, S., Strömberg, JE. (1994). From physical modelling to compositional models of hybrid systems. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_185
Download citation
DOI: https://doi.org/10.1007/3-540-58468-4_185
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58468-1
Online ISBN: 978-3-540-48984-9
eBook Packages: Springer Book Archive