The application of interval logic and modified labelled-net models for system specification and verification is introduced. By means of interval logic and modified labelled-net models, system properties involving time interval information can be specified and verified. In interval logic, derivation rules are used to obtain the criteria on the time relationships for the correct implementation of the system. The verification of system properties by derivation rules can be performed in the net space by net transformations which can be handled by an interactive computer. The human decision to select an appropriate net transformation rule is indispensable. Token passing is used to verify that the criteria for correct implementation are met by the parameters of a given set of components. An offline program without human intervention may be used to perform this job. An application example of a microcomputer system is used to demonstrate the power of these models.