License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06191.3
URN: urn:nbn:de:0030-drops-6407
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/640/
Go to the corresponding Portal

Leuschel, Michael ; Bendisposto, Jens

Animating and Model Checking B Specifications with Higher-Order Recursive Functions

pdf-format:
06191.LeuschelMichael.ExtAbstract.640.pdf (0.6 MB)

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.

BibTeX - Entry

@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.dagstuhl.de/opus/volltexte/2006/640},
  URN =		{urn:nbn:de:0030-drops-6407},
  doi =		{10.4230/DagSemProc.06191.3},
  annote =	{Keywords: B-Method, Model Checking, Animation, Logic Programming, Visualization}
}

Keywords: B-Method, Model Checking, Animation, Logic Programming, Visualization
Collection: 06191 - Rigorous Methods for Software Construction and Analysis
Issue Date: 2006
Date of publication: 08.08.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI