A TEMPORAL LOGIC APPROACH TO OBJECT CERTIFICATION

A brief overview is made of the use of temporal logic formalisms for s pecifying and verifying concurrent systems in general and information systems in particular. The requirements imposed by object-orientation on such formalisms are examined. A logic is proposed fulfilling those requirements (except concerning non-monotonic features), allowing the uniform treatment of both local and global properties of systems with concurrent, interacting components organized in classes, and supportin g specialization. A semantics and a calculus (following an axiomatic, Hilbert style) are presented in detail. The calculus includes rules fo r the sound inheritance and reflection of theorems between classes. Pr actical aspects of the usage of such a logic for both specification an d verification are considered. To this end a set of metatheorems is pr ovided for expediting the proof of invariants. Finally, the need and a vailability of automatic theorem proving for systems querying is brief ly discussed.