Refinement sensitive formal semantics of state machines with persistent choice

File Description SizeFormat 
refinement-state-machines.pdfAccepted version329.11 kBAdobe PDFDownload
Title: Refinement sensitive formal semantics of state machines with persistent choice
Author(s): Fecher, H
Huth, M
Schmidt, H
Schoenborn, J
Item Type: Journal Article
Abstract: Modeling languages usually support two kinds of nondeterminism, an external one for interactions of a system with its environment, and one that stems from under-specification as familiar in models of behavioral requirements. Both forms of nondeterminism are resolvable by composing a system with an environment model and by refining under-specified behavior (respectively). Modeling languages usually dont support nondeterminism that is persistent in that neither the composition with an environment nor refinements of under-specification will resolve it. Persistent nondeterminism is used, e.g., for modeling faulty systems. We present a formal semantics for UML state machines enriched with an operator persistent choice that models persistent nondeterminism. This semantics is based on abstract models - μ-automata with a novel refinement relation - and a sound three-valued satisfaction relation for properties expressed in the μ-calculus. © 2009 Elsevier B.V. All rights reserved.
Publication Date: 1-Sep-2009
Citation: Electronic Notes in Theoretical Computer Science Vol.( 250 ) No.( 1 ) pp 71 - 86
URI: http://hdl.handle.net/10044/1/5788
Publisher Link: http://dx.doi.org/10.1016/j.entcs.2009.08.006
ISSN: 1571-0661
Publisher: Elsevier
Start Page: 71
End Page: 86
Copyright Statement: © 2009 Elsevier B.V. All rights reserved. NOTICE: this is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, VOL:250, ISSUE:1, (2009) DOI:10.1016/j.entcs.2009.08.006
Volume: 250
Appears in Collections:Quantitative Analysis and Decision Science



Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons