Symbolic Verification of Hybrid Systems supported by Mathematical Services (bibtex)

by Christoph Benzmüller, Corrado Giromini, Andreas Nonnengart

Abstract:

Verification of hybrid systems is a challenging task. Unlike many other verification methods the approach proposed in [nonnengart99] avoids approximations and operates directly on the original system specifications. This approach, however, requires the solution of non-trivial mathematical subtasks. We propose to model those kinds of subtasks that are suitable for being tackled with reasoning specialists as mathematical service requests to a network of service systems like the MathWeb Software Bus. So far we have identified the following candidates of mathematical service requests: the solution of differential equations, subsumption and consistency of sets of constraints. A further candidate can be the elimination of second order set variables with higher order theorem provers.

Reference:

Symbolic Verification of Hybrid Systems supported by Mathematical Services (Christoph Benzmüller, Corrado Giromini, Andreas Nonnengart), In Additonal Proceedings of 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2002), pp. 1-10, 2002. (Url (preprint): http://christoph-benzmueller.de/papers/W17.pdf)

Bibtex Entry:

@inproceedings{W17, Abstract = {Verification of hybrid systems is a challenging task. Unlike many other verification methods the approach proposed in [nonnengart99] avoids approximations and operates directly on the original system specifications. This approach, however, requires the solution of non-trivial mathematical subtasks. We propose to model those kinds of subtasks that are suitable for being tackled with reasoning specialists as mathematical service requests to a network of service systems like the MathWeb Software Bus. So far we have identified the following candidates of mathematical service requests: the solution of differential equations, subsumption and consistency of sets of constraints. A further candidate can be the elimination of second order set variables with higher order theorem provers.}, Address = {Marseilles, France}, Author = {Christoph Benzm{\"u}ller and Corrado Giromini and Andreas Nonnengart}, Booktitle = {Additonal Proceedings of 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2002)}, Pages = {1-10}, Title = {Symbolic Verification of Hybrid Systems supported by Mathematical Services}, Note = {Url (preprint): \url{http://christoph-benzmueller.de/papers/W17.pdf}}, Year = 2002, }

Powered by bibtexbrowser