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. (Url (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},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/W18.pdf}},
  Year =	 2002,
}
Powered by bibtexbrowser