@inproceedings{39061,
  abstract     = {{This article presents an approach, which combines theorem proving-based refinement with model checking for state based real-time systems. Our verification flow starts from UML state diagrams, which are translated to the formal B language and are model checked for real-time properties. By means of the B language and a B theorem prover, refined state diagrams are verified against their abstract representation. The approach is presented by means of the refinement of a digital echo cancellation unit.}},
  author       = {{Krupp, Alexander and Müller, Wolfgang and Oliver, Ian}},
  booktitle    = {{Proceedings of DATE’04 Designers' Forum}},
  isbn         = {{0-7695-2085-5}},
  keywords     = {{Echo cancellers, Logic, Unified modeling language, Automata, Data structures, Boolean functions, Electronic design automation and methodology, Prototypes, Specification languages, Constraint theory}},
  title        = {{{Formal Refinement and Model Checking of An Echo Cancellation Unit}}},
  doi          = {{10.1109/DATE.2004.1269214}},
  year         = {{2004}},
}

@inproceedings{39421,
  abstract     = {{We present a rigorous but transparent semantics definition of SystemC that covers method, thread, and clocked thread behavior as well as their interaction with the simulation kernel process. The semantics includes watching statements, signal assignment, and wait statements as they are introduced in SystemC V1.O. We present our definition in form of distributed Abstract State Machines (ASMs) rules reflecting the view given in the SystemC User's Manual and the reference implementation. We mainly see our formal semantics as a concise, unambiguous, high-level specification for SystemC-based implementations and for standardization. Additionally, it can be used as a sound basis to investigate SystemC interoperability with Verilog and VHDL.}},
  author       = {{Müller, Wolfgang and Ruf, Jürgen and Hoffmann, D. W. and Gerlach, Joachim and Kropf, Thomas and Rosenstiehl, W.}},
  booktitle    = {{Proceedings of the Design, Automation, and Test in Europe (DATE’01)}},
  isbn         = {{0-7695-0993-2}},
  keywords     = {{Yarn, Formal verification, Kernel, Hardware design languages, Electronic design automation and methodology, Algebra, Computational modeling, Logic functions, Computer languages, Clocks}},
  publisher    = {{IEEE}},
  title        = {{{The Simulation Semantics of SystemC}}},
  doi          = {{10.1109/DATE.2001.915002}},
  year         = {{2001}},
}