Temporal Logic Properties of Java Objects

ct 7 Applying finite-state verification techniques to software systems looks attractive because they are capable of detecting very subtle 8 defects in the logic design of these systems. Nevertheless, the integration of existing formal verification tools within programming 9 environments is not yet easy, mainly because of the semantic gap between widely used programming languages and the languages 10 used to describe system requirements. In this paper, we propose a formal requirement specification notation based on linear 11 temporal logic, with regard to object oriented program elements, such as classes and interfaces. The specification is inherently object 12 oriented and is meant for the verification of concurrent and distributed software systems. 13 Ó 2003 Published by Elsevier Science Inc.

• Type: Conference
• Year: 2001
• Where: SEKE
• Authors: Radu Iosif, Riccardo Sisto
• Keywords: Formal Verification Tools, SEKE 2001, Software Engineering, Software Systems, finite-state Verification Techniques