The Intuitionism Behind Statecharts Steps

Abstract

The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev, lacks compositionality. This report first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear, intuitionistic Kripke models, namely stabilization sequences. This yields, for the first time in the literature, a simple fully-abstract semantics which interprets Pnueli and Shalev's concept of failure naturally. The results not only give insight into the semantic subtleties of Statecharts, but also provide a basis for an implementation, for developing algebraic theories for macro steps, and for comparing different Statecharts variants.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 2000
Accession Number
ADA381480

Entities

People

  • Gerald Luettgen
  • Michael Mendler

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Chain Reactions
  • Chemical Reactions
  • Coding
  • Computer Science
  • Computers
  • Consistency
  • Construction
  • Electronic Mail
  • Engineering
  • Environment
  • Hierarchies
  • Language
  • Models
  • Notation
  • Software Development
  • Standards

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.