Abstract
This paper reports on system level modeling 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 modeling 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.