published papers

Harald Fecher and Jens Schönborn.
UML 2.0 state machines: Complete formal semantics via core state machines.

UML has become the standard modeling language for object-oriented systems. The informal description of UML and its continuous extension cause many ambiguities. Therefore, a formal semantics for UML is necessary, especially for formal reasoning and tool development. We present a formal semantics of UML 2.0 state machines, which are used for modeling the reactive behavior of objects, by (i) deriving core state machines with fewer design features and a precise syntax, (ii) developing a formal semantics for core state machines, and (iii) presenting a complete transformation from UML 2.0 state machines to core state machines. Such a transformational approach provides the opportunity of easy adaption to future changes of the semantics of UML state machines.

Harald Fecher and Michael Huth.
More precise partition abstraction.

We define, for any partition of a state space and for formulas of the modal μ-calculus, two variants of precision for abstractions that have that partition set as state space. These variants are defined via satisfaction parity games in which the Refuter can replace a concrete state with any state in the same partition before, respectively after, a quantifier move. These games are independent of the kind of abstraction. Our first variant makes the abstraction games of de Alfaro et al. model-independent, captures the definition of precision given by Shoham & Grumberg, and corresponds to generalized Kripke modal transition systems. Our second variant is then shown, for a fixed abstraction function, to render more precise abstractions through μ-automata without fairness. We discuss tradeoffs of both variants in terms of the size of abstractions, the perceived cost of their synthesis via theorem provers, and the preservation of equations that are valid over concrete models. Finally, we sketch a combination of both abstraction methods.

Harald Fecher and Michael Huth.
Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise.

Predicate abstraction frameworks are a powerful means of combating the state explosion problem in model checking as they automatically synthesize abstract models that either verify compliance with a property, give rise to a genuine counter-example or produce a spurious counter-example that drives refinement of the abstract model. Prominent tools for safety (e.g. Blast) and termination (e.g. Terminator) checking rely on this approach. This paper presents such an abstraction framework for all properties of the modal μ-calculus based on ranked predicate abstraction. We show that our framework is incremental and confluent and should therefore allow good refinement heuristics. Moreover, ranked predicate abstractions are proved to be precise (i.e. optimal as abstractions) and also complete in that all properties true in a model are also true in a finite-state, ranked predicate abstraction of that model. This completeness relates to known characterizations of relative completeness for predicate abstraction with branching time.

Sharon Shoham and Harald Fecher.
Local abstraction-refinement for the mu-calculus.

Counterexample-guided abstraction refinement (CEGAR) is a key technique for the verification of computer programs. Grumberg et al. developed a CEGAR-based algorithm for the modal mu-calculus. There, every abstract state is split in a refinement step. In this paper, the work of Grumberg et al. is generalized by presenting a new CEGAR-based algorithm for the mu-calculus. It is based on a more expressive abstract model and applies refinement only locally (at a single abstract state), i.e., the lazy abstraction technique for safety properties is adapted to the mu-calculus. Furthermore, it separates refinement determination from the (3-valued based) model checking. Three different heuristics for refinement determination are presented and illustrated.

Harald Fecher and Immo Grabe.
Finite Abstract Models for Deterministic Transition Systems: Fair Parallel Composition and Refinement-Preserving Logic.

Since usually no scheduler is given at the programming or modeling language level, abstract models together with a refinement notion are necessary to model concurrent systems adequately. Deterministic transition systems are an appropriate model for implementations of (concurrent) reactive programs based on synchronous communication. In this paper, we develop a suitable setting for modeling and reasoning about deterministic transition systems. In particular, we (i) develop a class of abstract models together with a refinement notion; (ii) define parallel composition guaranteeing fairness; and (iii) develop a 3-valued logic with a satisfaction relation that is preserved under refinement.

Harald Fecher and Heiko Schmidt.
Process Algebra Having Inherent Choice: Revised Semantics for Concurrent Systems.

Process algebras are standard formalisms for compositionally describing systems by the dependencies of their observable synchronous communication. In concurrent systems, parallel composition introduces resolvable nondeterminism, i.e., nondeterminism that will be resolved in later design phases or by the operating system. Sometimes it is also important to express inherent nondeterminism for equal (communication) labels. Here, we give operational and axiomatic semantics to a process algebra having a parallel operator interpreted as concurrent and having a choice operator interpreted as inherent, not only with respect to different, but also with respect to equal next-step actions. In order to handle the different kinds of nondeterminism, the operational semantics uses mu-automata as underlying semantical model. Soundness and completeness of our axiom system with respect to the operational semantics is shown.

Harald Fecher, Michael Huth, Heiko Schmidt and Jens Schönborn
Refinement sensitive formal semantics of state machines with persistent choice

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 don’t 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.

Heiko Schmidt and Harald Fecher.
Comparing Disjunctive Modal Transition Systems with an One-Selecting Variant.

Abstract models, used for specification, analysis and verification, usually describe sets of implementations by means of a refinement relation. In the branching time setting, implementations are commonly modeled as labeled transition systems (LTS). An expressive class of abstractions for LTSs is that of disjunctive modal transition systems (DMTS), featuring may- and must transitions as well as disjunctive hypertransitions (OR). In order to describe exclusive choice adequately, we develop a variant of DMTSs called 1-selecting modal transition systems (1MTS) that, roughly speaking, interprets hypertransitions exclusively (XOR). These abstract models, DMTSs and 1MTSs, are compared with respect to their expressive power. By giving transformations or showing their non-existence, we show that the two settings can express the same sets of implementations, but 1-selecting modal transition systems have a richer refinement preorder.

Heiko Schmidt and Harald Fecher.
Comparing Disjunctive Modal Transition Systems with an One-Selecting Variant.

Harald Fecher and Michael Huth.
Complete Abstractions through Extensions of Disjunctive Modal Transition Systems.

Modal transition systems and their many variants are established models for abstraction and specification as they explicitly specify necessary and possible state or behavior. Disjunctive modal transition systems can be more precise abstractions as they allow a disjunctive split on necessary transitions. We show that these abstractions are compact, sound, and complete for - and as expressive as - the modal mu-calculus if models are enriched with fairness constraints and conjunctive splitting abilities for possible transitions. We point out the potential benefits of our approach over other complete abstraction frameworks.

download: [pdf-file]

Harald Fecher, Heiko Schmidt and Jens Schönborn.
UML state machines: Fairness Conditions specify the Event Pool.

The communication between different instances of UML state machines is handled by using underlying event pools but the UML standard leaves the behavior completely unspecifed. Thus, in general, liveness properties cannot be verifed. We give semantics of Streett fairness constraints for the event pool and present an algorithm that turns a set of fairness constraints into an abstract event pool. Since common fairness suffers from the drawback that the time until something good happens may be unbounded the presented algorithm allows the modeler to specify such a bound. The resulting abstract event pool can be further refined, justied by an example where a priority scheme on events is introduced.