Combining Interval Arithmetic and Three-Valued Temporal Logics for the Verification of Analog Systems
In: Christian Haubelt and Jürgen Teich ed., Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. Shaker Verlag, Aachen, Germany, P. 121--130, 10. Workshop MBMV '07, March, 2007
Authors
- Raffaella Gentilini
- Klaus Schneider
- Alexander Dreyer
Abstract
We deal with the problem of designing suitable languages for the modeling and the automatic verification of properties over analog circuits. To this purpose, we suitably enrich classical temporal logics with basic formulæ allowing to model arbitrary functions relating analog variables. We show how to accomplish the task of automatically check the resulting CTLf formulae on analog circuits. To this purpose, we extend to the analog context a number of techniques for the abstraction and the verification of digital systems, based on three-valued temporal logics.
Full Text
BibTeX
@InProceedings{ GentilinSchneiderDreyer07,
title = { Combining Interval Arithmetic and Three-Valued Temporal Logics for the Verification of Analog Systems },
author = { Raffaella Gentilini and Klaus Schneider and Alexander Dreyer },
editor = { Christian Haubelt and Jürgen Teich },
booktitle = { Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen },
publisher = { Shaker Verlag, Aachen, Germany },
pages = { 121--130 },
note = { 10. Workshop MBMV '07 },
month = mar,
year = 2007,
}
This publication belongs to the project
VerSiS.
