Research of Modeling and Verification of Component-based Real-time System
Using component based software design method in complex real-time system development has become a hot research topic.Verify whether the real-time software meets the given time requirement and reduce the complexity of the verification process is one of the main challenges in real-time computing research area.This paper proposes timed interface model and using it for formal modeling the interactions between component interfaces.Based on interface automata theory the timed interface automata is proposed and used to describe the action and composition of components under the interaction of timed interface.To cope with state space exploration problem,the product of timed interface automata models of components is reduced by eliminating incorrect states before verifying related properties.A simple example through this paper is studied in detail to illustrate how to apply the proposed approach.