Abstract:Based on a formal method called Abstract State Machine (ASM), this paper describes an admission control mechanism of real-time task in resource-sharing network. In the meantime, the paper also proposes an ASM-based design model for executable probability of real-time task, and shows the methods and steps to analyze this design model based on Spec Explorer. The paper argues that the work will not only do good to further verification for the design method, but also to more refinements for admission control of real-time task. And the ASM model also provides an example for the realization of other control mechanisms designed.