System level models for real-time communication
P.H.A. van der Putten, Jeroen P. M. Voeten, Marc C. W. Geilen, M.P.J. Stevens · Proceedings 25th EUROMICRO Conference. Informatics: Theory and Practice for the New Millennium · 1999
This paper reports on system level modelling techniques for specification and verification of real-time distributed systems. The approach uses an object-oriented description technique that yields formal executable system level models, suitable for hardware/software co-specification. The focus in this paper is on finding system level abstractions for modelling real-time communication in distributed systems. A generic LAN model is presented that models the properties of tightness, bounded transmission delay, and bounded omission degree. The model is evaluated for the quality of verification of real-time properties. This leads to the definition of research goals in new fields of formal verification, such as time continuous qualitative property verification, and probabilistic quantitative verification.