WestminsterResearch

Handling periodic properties: deductive verification for quantified temporal logic specifications

Bolotov, Alexander (2011) Handling periodic properties: deductive verification for quantified temporal logic specifications. In: 2011 5th international conference on secure software integration and reliability improvement companion. IEEE, pp. 179-186. ISBN 9781457707810

Full text not available from this repository.

Official URL: http://dx.doi.org/10.1109/SSIRI-C.2011.41

Abstract

We present a deductive verification technique for the specifications written in terms of quantified propositional linear-time temporal logic (QPTL). The system extends previous natural deduction constructions for the propositional linear-time temporal logic. Our result expands the applicability of the natural deduction based verification in the temporal setting to more sophisticated specifications due to the expressive power of QPTL, which is equivalent to Buchi Automata. In particular, the paper introduces a novel formal framework to verify specifications of a larger set of useful periodic properties that are particularly important to maintain during different cycles of software integration. Moreover, the novel elegant and succinct natural deduction based verification method enables tracing the dependency of the verified properties on the assumptions of the underlying model and brings prospects for automation.

Item Type:Book Section
Research Community:University of Westminster > Electronics and Computer Science, School of
ID Code:10951
Deposited On:27 Jul 2012 12:05
Last Modified:27 Jul 2012 12:05

Repository Staff Only: item control page