Procedure-level verification of real-time concurrent systems

Abstract

We want to develop verification techniques for real-time concurrent system specifications with high-level behavior structures. Nowadays, there is a big gap in between the classical verification theories and the engineering practice in real-world projects. This work identifies two 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 group of statements, allows local state space search to exploit the local autonomy in concurrent systems without calculating the Cartesian products of local state spaces, and derives from each procedure declaration characteristic 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 version of a real-world protocol in a mobile communication environment, and report the data.