Developer-friendly verification of process-based systems

Autor(en): Pulvermueller, Elke 
Feja, Sven
Speck, Andreas
Stichwörter: Business process verification; CHECKING; Computer Science; Computer Science, Artificial Intelligence; Extended temporal logic; Graphical result presentation; Graphical specification; MODEL; Model checking; User-friendliness
Erscheinungsdatum: 2010
Herausgeber: ELSEVIER
Journal: KNOWLEDGE-BASED SYSTEMS
Volumen: 23
Ausgabe: 7, SI
Startseite: 667
Seitenende: 676
Zusammenfassung: 
System quality is a key issue in modern systems development. Tool support is essential for checking the system quality efficiently. This is particularly true with respect to the dynamic interactions of the processes within a system. A first generation of checkers - model checkers - provide a basic technology for the verification of process-based systems. Conventional model checkers bear two drawbacks concerning mainly their user-friendliness which impede their broad application. First, model checkers in general do not support the graphical representation of rules (specifications). Although a model may be described with a graphical notation, the specification which has to be checked against the model is generally still text-based. This makes the usage of the checker difficult for process modeling experts. Second, the expressiveness concerning the verification model semantics to be checked is limited to states which are connected by transitions. However, many system development models (e.g. the business process model we use as example) embrace more element types. These are unsupported by the conventional model checkers resulting in a loss of verification precision. The checking system we present in this paper integrates both novelties: the graphical notation for a user-friendly specification and an extended specification language together with a corresponding verifier which supports the checking of many different types of elements (although the paper presents the approach with only two types). The integration is realized by an XML-based transformation system which links the graphical editor to the checking tool. (C) 2010 Elsevier B.V. All rights reserved.
ISSN: 09507051
DOI: 10.1016/j.knosys.2010.03.005

Show full item record

Page view(s)

1
Last Week
0
Last month
0
checked on Feb 23, 2024

Google ScholarTM

Check

Altmetric