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 9781457707810Full text not available from this repository.
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|
|Subjects:||University of Westminster > Science and Technology > Electronics and Computer Science, School of (No longer in use)|
|Depositing User:||Rachel Wheelhouse|
|Date Deposited:||27 Jul 2012 11:05|
|Last Modified:||27 Jul 2012 11:05|
Actions (login required)
|Edit Item (Repository staff only)|