Search Results

Documents authored by Leuschel, Michael

Document
DOI: 10.4230/DagRep.3.9.74
Integration of Tools for Rigorous Software Construction and Analysis (Dagstuhl Seminar 13372)

Authors: Uwe Glässer, Stefan Hallerstede, Michael Leuschel, and Elvinia Riccobene

Published in: Dagstuhl Reports, Volume 3, Issue 9 (2014)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13372 "Integration of Tools for Rigorous Software Construction and Analysis". The 32 participants came from 10 countries: Australia, Austria, Brazil, Canada, Denmark, France, Germany, Great Britain, Italy, Norway. The aim of the seminar was to bring together researchers and tool developers from different state- and machine-based formal methods communities in order to share expertise and promote the joint use of modelling tool technologies. Indeed, each of these communities -- from Abstract State Machines, to B, TLA, VDM, Z -- has valuable tools and technologies which would be beneficial also for the other formal approaches. Understanding and clarifying their commonalities and differences is a key factor to achieve a possible integration or integrated use of these related approaches for accomplishing, in a rigorous way, the various modelling and analysis tasks to construct reliable high quality software systems. The working group formula offered by the Dagstuhl seminar was a fruitful way to share knowledge of the various techniques and tools -- such as simulators, animators, model checkers, theorem proves -- developed for the individual methods, and to constructively experiment the combined use of different approaches by means of a series of well known case studies. Participants did not arrive with well-prepared solutions, but all the modelling and integration work was directly done in Dagstuhl in a very exciting and competitive atmosphere. Some related presentation were also given on recent advances on methodologies and tools. The seminar posed the bases for a series of future research collaborations between different, and up to know closed, formal method communities. An LNCS volume will be prepared by the contributions of the all participants to give the common vision of future methodology and tool integration.
Cite as

Uwe Glässer, Stefan Hallerstede, Michael Leuschel, and Elvinia Riccobene. Integration of Tools for Rigorous Software Construction and Analysis (Dagstuhl Seminar 13372). In Dagstuhl Reports, Volume 3, Issue 9, pp. 74-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{glasser_et_al:DagRep.3.9.74,
  author =	{Gl\"{a}sser, Uwe and Hallerstede, Stefan and Leuschel, Michael and Riccobene, Elvinia},
  title =	{{Integration of Tools for Rigorous Software Construction and Analysis (Dagstuhl Seminar 13372)}},
  pages =	{74--105},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{9},
  editor =	{Gl\"{a}sser, Uwe and Hallerstede, Stefan and Leuschel, Michael and Riccobene, Elvinia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.9.74},
  URN =		{urn:nbn:de:0030-drops-43584},
  doi =		{10.4230/DagRep.3.9.74},
  annote =	{Keywords: Applied Formal Methods; Modelling Formalisms; Modelling Tools; Abstract State Machines; B Method; Event-B; TLA+; VDM; Z; Verification; Validation; Proof; Simulation; Animation; Visualisation; Model-Checking; Tool Integration}
}
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.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}
}
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