Procedure-level verification of real-time concurrent systems

We want to develop verification techniques for real-time concurrent system specifications with high-level behavior structures. This work identifies tw o common engineering guidelines respected in the development of real-world software projects, structured programming and local autonomy in concurrent systems, and experiments with special verification algorithm based on those engineering wisdoms. The algorithm we have adopted respects the integrity of program structures, treats each procedure as an entity instead of as a g roup of statements, allows local state space search to exploit the local au tonomy in concurrent systems without calculating the Cartesian products of local state spaces, and derives from each procedure declaration characteris tic information which can be utilized in the verification process anywhere the procedure is invoked. We have endeavored to implement our idea, test it against an abstract extension of a real-world protocol in a mobile communi cation environment, and report the data.