Coarse-granular model checking in practice

Bernhard Steffen, Tiziana Margaria, Volker Braun

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

In this paper, we illustrate the power of 'classical' iterative model checking for verifying quality of service requirements at the coarse granular level. Characteristic for our approach is the library-based modelling of applications in terms of service logic graphs, the incremental formalization of the underlying application domain in terms of temporal quality of service constraints, and the library-based consistency checking allowing continuous verification of application- and purpose-specific properties by means of model checking. This enables application experts to safely configure their own applications without requiring any specific knowledge about the underlying technology. The impact of this approach will be demonstrated in three orthogonal industrial application scenarios.

Original languageEnglish
Title of host publicationModel Checking Software - 8th International SPIN Workshop, Proceedings
EditorsMatthew Dwyer
PublisherSpringer Verlag
Pages304-311
Number of pages8
ISBN (Print)3540421246, 9783540421245
DOIs
Publication statusPublished - 2001
Externally publishedYes
Event8th International SPIN Workshop on Model Checking Software, SPIN 2001 - Toronto, ON, Canada
Duration: 19 May 200120 May 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2057 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International SPIN Workshop on Model Checking Software, SPIN 2001
Country/TerritoryCanada
CityToronto, ON
Period19/05/0120/05/01

Fingerprint

Dive into the research topics of 'Coarse-granular model checking in practice'. Together they form a unique fingerprint.

Cite this