1 Search Results for "Bendisposto, Jens"

Document
DOI: 10.4230/DagSemProc.06191.3
Animating and Model Checking B Specifications with Higher-Order Recursive Functions

Authors: Michael Leuschel and Jens Bendisposto

Published in: Dagstuhl Seminar Proceedings, Volume 6191, Rigorous Methods for Software Construction and Analysis (2006)

Abstract
Real-life specifications often contain complicated functions. Animation and validation of such functions and specifications is very important. However, such functions pose a major challenge to animation and model checking. Earlier versions of ProB required that functions be explicitly expanded which is prohibitively expensive or impossible. The central idea of this new research is to compile such functions into symbolic closures which are only examined when the function is applied to some particular argument. This enables ProB to successfully animate and model check a new class of specifications, where animation is especially important due to the involved nature of the specification. We will illustrate this new approach on an industrial case study.
Cite as

Michael Leuschel and Jens Bendisposto. Animating and Model Checking B Specifications with Higher-Order Recursive Functions. In Rigorous Methods for Software Construction and Analysis. Dagstuhl Seminar Proceedings, Volume 6191, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{leuschel_et_al:DagSemProc.06191.3,
  author =	{Leuschel, Michael and Bendisposto, Jens},
  title =	{{Animating and Model Checking B Specifications with Higher-Order Recursive Functions}},
  booktitle =	{Rigorous Methods for Software Construction and Analysis},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6191},
  editor =	{Jean-Raymond Abrial and Uwe Gl\"{a}sser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06191.3},
  URN =		{urn:nbn:de:0030-drops-6407},
  doi =		{10.4230/DagSemProc.06191.3},
  annote =	{Keywords: B-Method, Model Checking, Animation, Logic Programming, Visualization}
}
  • Refine by Author
  • 1 Bendisposto, Jens
  • 1 Leuschel, Michael

  • Refine by Classification

  • Refine by Keyword
  • 1 Animation
  • 1 B-Method
  • 1 Logic Programming
  • 1 Model Checking
  • 1 Visualization

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2006

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact