×

A temporal logic approach to object certification\(^{\star}\). (English) Zbl 0875.68788

Summary: A brief overview is made of the use of temporal logic formalisms for specifying 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 supporting specialization. A semantics and a calculus (following an axiomatic, Hilbert style) are presented in detail. The calculus includes rules for the sound inheritance and reflection of theorems between classes. Practical aspects of the usage of such a logic for both specification and verification are considered. To this end a set of metatheorems is provided for expediting the proof of invariants. Finally, the need and availability of automatic theorem proving for systems querying is briefly discussed.

MSC:

68T27 Logic in artificial intelligence
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B45 Modal logic (including the logic of norms)
PDFBibTeX XMLCite
Full Text: DOI