Procedure-Level Verification of Real-time Concurrent Systems.
Journal
FME '96: Industrial Benefit and Advances in Formal Methods, Third International Symposium of Formal Methods Europe, Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18-22, 1996, Proceedings
Pages
682-701
Date Issued
1996
Author(s)
Lo, Chia-Tien Dan
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. © Springer-Verlag Berlin Heidelberg 1996.
Other Subjects
Formal methods; Search engines; Specifications; Structured programming; Verification; Engineering guidelines; Engineering practices; Mobile communications; Real time concurrent systems; Real world projects; Verification algorithms; Verification process; Verification techniques; Real time systems
Type
conference paper