Reasoning Services in the MathWeb-SB for Symbolic Verification of Hybrid Systems (bibtex)

by Christoph Benzmüller, Corrado Giromini, Andreas Nonnengart, Jürgen Zimmer

Abstract:

Verification of non-linear hybrid systems is a challenging task. Unlike many other verification methods the deduction-based verification approach we investigate in this paper avoids approximations and operates directly on the original non-linear system specifications. This approach, however, requires the solution of non-trivial mathematical subtasks. We propose to model existing reasoning systems, such as computer algebra systems and constraint solvers, as mathematical services and to provide them in a network of mathematical tools in a way that they can reasonably support subtasks as they may occur in formal methods applications. The motivation is to make it simpler to implement and test verification approaches by out-sourcing complex but precisely identifiable mathematical subtasks for which specialised reasoners do already exists.

Reference:

Reasoning Services in the MathWeb-SB for Symbolic Verification of Hybrid Systems (Christoph Benzmüller, Corrado Giromini, Andreas Nonnengart, Jürgen Zimmer), In Proceedings of the Verification Workshop - VERIFY'02 in connection with FLOC 2002, pp. 29-39, 2002. (Preprint: http://christoph-benzmueller.de/papers/W18.pdf)

Bibtex Entry:

@inproceedings{W18, Abstract = {Verification of non-linear hybrid systems is a challenging task. Unlike many other verification methods the deduction-based verification approach we investigate in this paper avoids approximations and operates directly on the original non-linear system specifications. This approach, however, requires the solution of non-trivial mathematical subtasks. We propose to model existing reasoning systems, such as computer algebra systems and constraint solvers, as mathematical services and to provide them in a network of mathematical tools in a way that they can reasonably support subtasks as they may occur in formal methods applications. The motivation is to make it simpler to implement and test verification approaches by out-sourcing complex but precisely identifiable mathematical subtasks for which specialised reasoners do already exists.}, Address = {Kopenhagen, Denmark}, Author = {Christoph Benzm{\"u}ller and Corrado Giromini and Andreas Nonnengart and J{\"u}rgen Zimmer}, Booktitle = {Proceedings of the Verification Workshop - VERIFY'02 in connection with FLOC 2002}, Pages = {29-39}, Title = {Reasoning Services in the MathWeb-SB for Symbolic Verification of Hybrid Systems}, Addendum = {Preprint: \url{http://christoph-benzmueller.de/papers/W18.pdf}}, Year = 2002, }