@InProceedings{Hilderink06,
  title =        "{S}oftware {S}pecification {R}efinement and {V}erification {M}ethod with {I}-{M}athic {S}tudio.",
  author=        "Hilderink,  Gerald H.",
  editor=        "Welch, Peter H. and Kerridge,  Jon and Barnes,  Frederick R. M.",
  pages =        "297--310",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2006",
  isbn=          "978-1-58603-671-3",
  year=          "2006",
  month=         "sep",
  abstract=      "A software design usually manifests a composition of
     software specifications. It consists of hierarchies of black
     box and white box specifications which are subject to
     refinement verification. Refinement verification is a
     model-checking process that proves the correctness of
     software specifications using formal methods. Although this
     is a powerful tool for developing reliable and robust
     software, the applied mathematics causes a serious gap
     between academics and software engineers. I-Mathic
     comprehends a software specification refinement and
     verification method and a supporting toolset, which aims at
     eliminating the gap through hiding the applied mathematics
     by practical modelling concepts. The model-checker FDR is
     used for refinement verification and detecting deadlocks and
     livelocks in software specifications. We have improved the
     method by incorporating CSP programming concepts into the
     specification language. These concepts make the method
     suitable for a broader class of safety-critical concurrent
     systems. The improved I-Mathic is illustrated in this paper."
}