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